Merge pull request #202 from ryukzak/72-integrity

Check integrity for process units

nitta.cabal

@@ -59,6 +59,7 @@ library
       NITTA.Model.Problems.Refactor.OptimizeAccum
       NITTA.Model.Problems.Refactor.ResolveDeadlock
       NITTA.Model.Problems.ViewHelper
+      NITTA.Model.ProcessIntegrity
       NITTA.Model.ProcessorUnits
       NITTA.Model.ProcessorUnits.Accum
       NITTA.Model.ProcessorUnits.Broken

src/NITTA/Model/Networks/Bus.hs

@@ -25,6 +25,7 @@ For creating BusNetwork see 'NITTA.Model.Microarchitecture.Builder'.
 -}
 module NITTA.Model.Networks.Bus (
     BusNetwork (..),
+    Instruction (..),
     Ports (..),
     IOPorts (..),
     bindedFunctions,
@@ -193,8 +194,8 @@ instance (UnitTag tag, VarValTime v x t) => ProcessorUnit (BusNetwork tag v x t)
         let v2transportStepKey =
                 M.fromList
                     [ (v, pID)
-                    | Step{pID, pDesc} <- steps bnProcess
-                    , isInstruction pDesc
+                    | step@Step{pID, pDesc} <- steps bnProcess
+                    , isInstruction step
                     , v <- case pDesc of
                         (InstructionStep ins) | Just (Transport var _ _) <- castInstruction net ins -> [var]
                         _ -> []
@@ -216,7 +217,7 @@ instance (UnitTag tag, VarValTime v x t) => ProcessorUnit (BusNetwork tag v x t)
                 mapM_
                     ( \(epKey, v) ->
                         when (v `M.member` v2transportStepKey) $
-                            establishVerticalRelation (v2transportStepKey M.! v) epKey
+                            establishVerticalRelations [v2transportStepKey M.! v] [epKey]
                     )
                     enpointStepKeyVars
 
@@ -226,7 +227,7 @@ instance (UnitTag tag, VarValTime v x t) => ProcessorUnit (BusNetwork tag v x t)
                         mapM_
                             ( \v ->
                                 when (v `M.member` v2transportStepKey) $
-                                    establishVerticalRelation pID (v2transportStepKey M.! v)
+                                    establishVerticalRelations [pID] [v2transportStepKey M.! v]
                             )
                             $ variables f
                     )
@@ -243,7 +244,12 @@ instance (UnitTag tag, VarValTime v x t) => ProcessorUnit (BusNetwork tag v x t)
                                 return (pID, pID')
                             )
                             steps
-                mapM_ (\(Vertical h l) -> establishVerticalRelation (pu2netKey M.! h) (pu2netKey M.! l)) relations
+                mapM_
+                    ( \case
+                        (Vertical h l) -> establishVerticalRelations [pu2netKey M.! h] [pu2netKey M.! l]
+                        (Horizontal h l) -> establishHorizontalRelations [pu2netKey M.! h] [pu2netKey M.! l]
+                    )
+                    relations
 
 instance Controllable (BusNetwork tag v x t) where
     data Instruction (BusNetwork tag v x t)

src/NITTA/Model/Problems/Dataflow.hs

@@ -27,7 +27,7 @@ import GHC.Generics
 import NITTA.Intermediate.Variable
 import NITTA.Model.Problems.Endpoint
 import NITTA.Model.Time
-import NITTA.Utils
+import NITTA.Utils.Base
 import Numeric.Interval.NonEmpty
 
 {- |Dataflow option (@tp ~ TimeConstraint t@) or decision (@tp Z Interval t@)

src/NITTA/Model/ProcessIntegrity.hs

@@ -0,0 +1,96 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{- |
+Module      : NITTA.Model.ProcessIntegrity
+Description : Checking the target process integrity
+Copyright   : (c) Artyom Kostyuchik, Aleksandr Penskoi, 2022
+License     : BSD3
+Maintainer  : aleksandr.penskoi@gmail.com
+Stability   : experimental
+-}
+module NITTA.Model.ProcessIntegrity (
+    ProcessIntegrity (checkProcessIntegrity),
+    isProcessIntegrity,
+) where
+
+import Data.Either
+import qualified Data.List as L
+import qualified Data.Map.Strict as M
+import Data.Maybe
+import qualified Data.Set as S
+import qualified Data.String.Utils as S
+import NITTA.Model.ProcessorUnits
+import NITTA.Utils
+
+class ProcessIntegrity u where
+    checkProcessIntegrity :: u -> Either String ()
+
+isProcessIntegrity u = isRight $ checkProcessIntegrity u
+
+instance (ProcessorUnit (pu v x t) v x t) => ProcessIntegrity (pu v x t) where
+    checkProcessIntegrity pu =
+        collectChecks
+            [ checkVerticalRelations (up2down pu) (pid2intermediate pu) (pid2endpoint pu) "intermediate not related to endpoint"
+            , checkVerticalRelations (down2up pu) (pid2endpoint pu) (pid2intermediate pu) "endpoint not related to intermediate"
+            , checkVerticalRelations (up2down pu) (pid2endpoint pu) (pid2instruction pu) "endpoint not related to instruction"
+            , checkVerticalRelations (down2up pu) (pid2instruction pu) (pid2endpoint pu) "instruction not related to endpoint"
+            ]
+
+checkVerticalRelations f dom codom errmsg =
+    collectChecks $
+        map
+            ( \x ->
+                let ys = M.findWithDefault S.empty x f
+                 in if any (`M.member` codom) $ S.elems ys
+                        then Right ()
+                        else Left $ errmsg <> ": " <> show (dom M.! x)
+            )
+            $ M.keys dom
+
+-- TODO: #205 Divider: missing vertical relation between Do instruction and Endpoint
+skipIntegrityErrors = ["instruction not related to endpoint: Instruction: Do"]
+
+collectChecks checks = case lefts checks of
+    [] -> Right ()
+    errs -> case filter (`L.notElem` skipIntegrityErrors) errs of
+        [] -> Right ()
+        errs' -> Left $ S.join "; " errs'
+
+relationsMap pairs = M.fromList $ map merge $ L.groupBy (\a b -> fst a == fst b) $ L.sortOn fst pairs
+    where
+        merge xs@((a, _) : _) = (a, S.fromList $ map snd xs)
+        merge _ = error "internal error"
+
+up2down pu = relationsMap $ mapMaybe get $ relations $ process pu
+    where
+        get Vertical{vUp, vDown} = Just (vUp, vDown)
+        get _ = Nothing
+
+down2up pu = relationsMap $ mapMaybe get $ relations $ process pu
+    where
+        get Vertical{vUp, vDown} = Just (vDown, vUp)
+        get _ = Nothing
+
+pid2intermediate pu = M.fromList $ mapMaybe get $ steps $ process pu
+    where
+        get s@Step{pID}
+            | Just f <- getFunction s = Just (pID, f)
+            | otherwise = Nothing
+
+pid2endpoint pu = M.fromList $ mapMaybe get $ steps $ process pu
+    where
+        get s@Step{pID}
+            | Just ep <- getEndpoint s = Just (pID, ep)
+            | otherwise = Nothing
+
+pid2instruction pu = M.fromList $ mapMaybe get $ steps $ process pu
+    where
+        get s@Step{pID}
+            | Just instr <- getInstruction s = Just (pID, instr)
+            | otherwise = Nothing

src/NITTA/Model/ProcessorUnits/Broken.hs

@@ -26,7 +26,7 @@ module NITTA.Model.ProcessorUnits.Broken (
     IOPorts (..),
 ) where
 
-import Control.Monad (when)
+import Control.Monad
 import Data.Default
 import Data.List (find, (\\))
 import Data.Set (elems, fromList, member)
@@ -66,6 +66,9 @@ data Broken v x t = Broken
     , -- |lost source endpoint due synthesis
       lostEndpointSource :: Bool
     , wrongAttr :: Bool
+    , lostFunctionInVerticalRelation :: Bool
+    , lostEndpointInVerticalRelation :: Bool
+    , lostInstructionInVerticalRelation :: Bool
     , unknownDataOut :: Bool
     }
 
@@ -149,17 +152,62 @@ instance (VarValTime v x t) => EndpointProblem (Broken v x t) v t where
                     , doneAt = Just $ sup epAt + 3
                     }
     endpointDecision
-        pu@Broken{targets = [], sources, doneAt, currentWork = Just (a, f), currentWorkEndpoints, wrongControlOnPull}
-        d@EndpointSt{epRole = Source v, epAt}
+        pu@Broken
+            { targets = [v]
+            , currentWorkEndpoints
+            , wrongControlOnPush
+            , lostEndpointInVerticalRelation
+            , lostInstructionInVerticalRelation
+            }
+        d@EndpointSt{epRole = Target v', epAt}
+            | v == v'
+              , let (newEndpoints, process_') = runSchedule pu $ do
+                        let ins =
+                                if lostInstructionInVerticalRelation
+                                    then return []
+                                    else scheduleInstructionUnsafe (shiftI (if wrongControlOnPush then 1 else 0) epAt) Load
+
+                        if lostEndpointInVerticalRelation
+                            then return []
+                            else scheduleEndpoint d ins =
+                pu
+                    { process_ = process_'
+                    , targets = []
+                    , currentWorkEndpoints = newEndpoints ++ currentWorkEndpoints
+                    , doneAt = Just $ sup epAt + 3
+                    }
+    endpointDecision
+        pu@Broken
+            { targets = []
+            , sources
+            , doneAt
+            , currentWork = Just (a, f)
+            , currentWorkEndpoints
+            , wrongControlOnPull
+            , lostFunctionInVerticalRelation
+            , lostEndpointInVerticalRelation
+            , lostInstructionInVerticalRelation
+            }
+        EndpointSt{epRole = epRole@(Source v), epAt}
             | not $ null sources
               , let sources' = sources \\ elems v
               , sources' /= sources
               , let (newEndpoints, process_') = runSchedule pu $ do
-                        endpoints <- scheduleEndpoint d $ scheduleInstructionUnsafe (shiftI (if wrongControlOnPull then 0 else -1) epAt) Out
+                        let doAt = shiftI (if wrongControlOnPull then 0 else -1) epAt
+                        -- Inlined: endpoints <- scheduleEndpoint d $ scheduleInstructionUnsafe doAt Out
+                        endpoints <- do
+                            high <- scheduleStep epAt $ EndpointRoleStep epRole
+                            low <- scheduleInstructionUnsafe doAt Out
+                            establishVerticalRelations
+                                (if lostEndpointInVerticalRelation then [] else high)
+                                (if lostInstructionInVerticalRelation then [] else low)
+                            return high
                         when (null sources') $ do
                             high <- scheduleFunction (a ... sup epAt) f
                             let low = endpoints ++ currentWorkEndpoints
-                            establishVerticalRelations high low
+                            establishVerticalRelations
+                                (if lostFunctionInVerticalRelation then [] else high)
+                                (if lostEndpointInVerticalRelation then [] else low)
                         return endpoints =
                 pu
                     { process_ = process_'
@@ -220,6 +268,9 @@ instance (Time t) => Default (Broken v x t) where
             , lostEndpointTarget = False
             , lostEndpointSource = False
             , wrongAttr = False
+            , lostFunctionInVerticalRelation = False
+            , lostEndpointInVerticalRelation = False
+            , lostInstructionInVerticalRelation = False
             , unknownDataOut = False
             }
 

src/NITTA/Model/ProcessorUnits/Divider.hs

@@ -25,6 +25,7 @@ module NITTA.Model.ProcessorUnits.Divider (
     IOPorts (..),
 ) where
 
+import Control.Monad
 import Data.Default
 import Data.List (partition)
 import qualified Data.List as L
@@ -217,7 +218,7 @@ instance (VarValTime v x t) => EndpointProblem (Divider v x t) v t where
                                 scheduleEndpoint_ d $ scheduleInstructionUnsafe epAt $ Load tag
                             }
     endpointDecision pu@Divider{jobs} d@EndpointSt{epRole = Source vs, epAt}
-        | ([job@WaitResults{results}], jobs') <- partition ((vs `S.isSubsetOf`) . variables) jobs =
+        | ([job@WaitResults{results, function}], jobs') <- partition ((vs `S.isSubsetOf`) . variables) jobs =
             let ([(tag, allVs)], results') = partition ((vs `S.isSubsetOf`) . snd) results
                 allVs' = allVs S.\\ vs
                 results'' = filterEmptyResults $ (tag, allVs') : results'
@@ -229,6 +230,8 @@ instance (VarValTime v x t) => EndpointProblem (Divider v x t) v t where
                     { jobs = jobs''
                     , process_ = execSchedule pu $ do
                         scheduleEndpoint_ d $ scheduleInstructionUnsafe epAt $ Out tag
+                        when (null jobs') $ do
+                            scheduleFunctionFinish_ [] function $ 0 ... sup epAt
                     }
     endpointDecision _pu d = error [i|incorrect decision #{ d } for Divider|]