never executed always true always false

    1 {-# LANGUAGE ConstraintKinds #-}
    2 {-# LANGUAGE FunctionalDependencies #-}
    3 {-# LANGUAGE GADTs #-}
    4 {-# LANGUAGE TypeFamilies #-}
    5 
    6 {- |
    7 Module      : NITTA.Model.Problems.Refactor.ResolveDeadlock
    8 Description : Refactoring for resolving deadlocks
    9 Copyright   : (c) Aleksandr Penskoi, 2021
   10 License     : BSD3
   11 Maintainer  : aleksandr.penskoi@gmail.com
   12 Stability   : experimental
   13 
   14 Possible deadlocks (recognized in 'NITTA.Model.Networks.Bus'):
   15 
   16 - selfsending;
   17 
   18 @
   19                     source1
   20     DoubleLoopOut--b1--+--b2--> DoubleLoopIn
   21                |       +------> Send
   22                |
   23                +------b3------> DoubleLoopIn
   24                     source2
   25 
   26     Possible buffers: b1, b2, b3
   27 @
   28 
   29 - classical deadlock betweeb two function on same PU.
   30 
   31 @
   32     a + b = c ---+----> c + d = e ---> e * c = f
   33                  |                         ^
   34                  +-------------b1----------+
   35 @
   36 
   37 ResolveDeadlock example:
   38 
   39 > ResolveDeadlock [a, b]
   40 
   41 before:
   42 
   43 > f1 :: (...) -> ([a, b])
   44 > f2 :: (a, ...) -> (...)
   45 > f3 :: (b, ...) -> (...)
   46 
   47 f1, f2 and f3 process on same process unit. In this case, we have deadlock,
   48 which can be fixed by insertion of buffer between functions.
   49 
   50 after:
   51 
   52 > f1 :: (...) -> ([a@buf])
   53 > buffer :: a@buf -> ([a, b])
   54 > f2 :: (a, ...) -> (...)
   55 > f3 :: (b, ...) -> (...)
   56 -}
   57 module NITTA.Model.Problems.Refactor.ResolveDeadlock (
   58     ResolveDeadlock (..),
   59     ResolveDeadlockProblem (..),
   60     resolveDeadlock,
   61     maxBufferStack,
   62 ) where
   63 
   64 import Data.Default
   65 import Data.Map.Strict qualified as M
   66 import Data.Set qualified as S
   67 import GHC.Generics
   68 import NITTA.Intermediate.Functions
   69 import NITTA.Intermediate.Types
   70 import NITTA.Utils.Base
   71 
   72 data ResolveDeadlock v x = ResolveDeadlock
   73     { newBuffer :: F v x
   74     , changeset :: Changeset v
   75     }
   76     deriving (Generic, Show, Eq)
   77 
   78 class ResolveDeadlockProblem u v x | u -> v x where
   79     resolveDeadlockOptions :: u -> [ResolveDeadlock v x]
   80     resolveDeadlockOptions _ = []
   81 
   82     resolveDeadlockDecision :: u -> ResolveDeadlock v x -> u
   83     resolveDeadlockDecision _ _ = error "not supported"
   84 
   85 resolveDeadlock :: (Var v, Val x) => S.Set v -> ResolveDeadlock v x
   86 resolveDeadlock buffered =
   87     let bufferI = bufferSuffix $ oneOf buffered
   88         bufferO = S.elems buffered
   89         diff = def{changeO = M.fromList $ map (\o -> (o, S.singleton bufferI)) bufferO}
   90      in ResolveDeadlock
   91             { newBuffer = buffer bufferI bufferO
   92             , changeset = diff
   93             }
   94 
   95 -- | The constant, which restrict maximum length of a buffer sequence.
   96 maxBufferStack = 2 :: Int