never executed always true always false
1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE PartialTypeSignatures #-}
3 {-# LANGUAGE TypeFamilies #-}
4
5 {- |
6 Module : NITTA.Synthesis.Method
7 Description : Synthesis method implementation.
8 Copyright : (c) Aleksandr Penskoi, 2021
9 License : BSD3
10 Maintainer : aleksandr.penskoi@gmail.com
11 Stability : experimental
12 -}
13 module NITTA.Synthesis.Method (
14 DefTree,
15 SynthesisMethod,
16 noSynthesis,
17 simpleSynthesisIO,
18 smartBindSynthesisIO,
19 obviousBindThreadIO,
20 topDownByScoreSynthesisIO,
21 allBestThreadIO,
22 stateOfTheArtSynthesisIO,
23 allBindsAndRefsIO,
24 bestStepIO,
25 SynthesisMethodConstraints,
26 ) where
27
28 import Data.Heap qualified as H
29 import Data.List qualified as L
30 import Data.Map.Strict qualified as M
31 import Data.Text (Text)
32 import Data.Typeable
33 import Debug.Trace
34 import NITTA.Model.Networks.Bus (BusNetwork)
35 import NITTA.Model.ProcessorUnits
36 import NITTA.Model.TargetSystem
37 import NITTA.Synthesis.Explore
38 import NITTA.Synthesis.Steps
39 import NITTA.Synthesis.Types
40 import NITTA.UIBackend.Types
41 import NITTA.Utils (maximumOn, minimumOn)
42 import Safe
43 import System.Log.Logger
44 import Text.Printf (printf)
45
46 {- | The constant, which restricts the maximum number of synthesis steps. Avoids
47 the endless synthesis process.
48 -}
49 stepLimit = 750 :: Int
50
51 noSynthesis :: BackendCtx tag v x t -> SynthesisMethod tag v x t
52 noSynthesis _ctx tree = do
53 infoM "NITTA.Synthesis" "noSynthesis"
54 return tree
55
56 -- | The most complex synthesis method, which embedded all another. That all.
57 stateOfTheArtSynthesisIO :: SynthesisMethodConstraints tag v x t => BackendCtx tag v x t -> SynthesisMethod tag v x t
58 stateOfTheArtSynthesisIO ctx tree = do
59 infoM "NITTA.Synthesis" $ "stateOfTheArtSynthesisIO: " <> show (sID tree)
60 l1 <- simpleSynthesisIO ctx tree
61 l2 <- smartBindSynthesisIO ctx tree
62 l3 <- bestThreadIO ctx stepLimit tree
63 l4 <- bestThreadIO ctx stepLimit =<< allBindsAndRefsIO ctx tree
64 l5 <- obviousGroupBindsIO ctx tree >>= tryAllGroupBindsByIO (bestThreadIO ctx stepLimit) ctx
65 return $ bestLeaf tree [l1, l2, l3, l4, l5]
66
67 -- | Schedule process by simple synthesis.
68 simpleSynthesisIO :: SynthesisMethodConstraints tag v x t => BackendCtx tag v x t -> SynthesisMethod tag v x t
69 simpleSynthesisIO ctx root = do
70 infoM "NITTA.Synthesis" $ "simpleSynthesisIO: " <> show (sID root)
71 lastObviousNode <- obviousBindThreadIO ctx root
72 allBestThreadIO ctx 1 lastObviousNode
73
74 smartBindSynthesisIO :: SynthesisMethodConstraints tag v x t => BackendCtx tag v x t -> SynthesisMethod tag v x t
75 smartBindSynthesisIO ctx tree = do
76 infoM "NITTA.Synthesis" $ "smartBindSynthesisIO: " <> show (sID tree)
77 tree' <- smartBindThreadIO ctx tree
78 allBestThreadIO ctx 1 tree'
79
80 bestThreadIO :: SynthesisMethodConstraints tag v x t => BackendCtx tag v x t -> Int -> SynthesisMethod tag v x t
81 bestThreadIO _ 0 node = return $ trace "bestThreadIO've reached the step limit!" node
82 bestThreadIO ctx limit tree = do
83 subForest <- positiveSubForestIO ctx tree
84 case subForest of
85 [] -> return tree
86 _ -> bestThreadIO ctx (limit - 1) $ maximumOn (defScore . sDecision) subForest
87
88 bestStepIO :: SynthesisMethodConstraints tag v x t => BackendCtx tag v x t -> SynthesisMethod tag v x t
89 bestStepIO ctx tree = do
90 subForest <- positiveSubForestIO ctx tree
91 case subForest of
92 [] -> error "all step is over"
93 _ -> return $ maximumOn (defScore . sDecision) subForest
94
95 obviousGroupBindsIO :: SynthesisMethodConstraints tag v x t => BackendCtx tag v x t -> SynthesisMethod tag v x t
96 obviousGroupBindsIO ctx tree = do
97 binds <- selectSubForestIO isObviousMultiBind ctx tree
98 maybe (return tree) (obviousGroupBindsIO ctx) $ bestDecision binds
99
100 tryAllGroupBindsByIO :: SynthesisMethodConstraints tag v x t => SynthesisMethod tag v x t -> BackendCtx tag v x t -> SynthesisMethod tag v x t
101 tryAllGroupBindsByIO method ctx tree = do
102 bindSubForest <- selectSubForestIO isMultiBind ctx tree
103 leafs <- mapM method bindSubForest
104 return $ bestLeaf tree leafs
105
106 obviousBindThreadIO :: SynthesisMethodConstraints tag v x t => BackendCtx tag v x t -> SynthesisMethod tag v x t
107 obviousBindThreadIO ctx tree = do
108 subForest <- positiveSubForestIO ctx tree
109 maybe (return tree) (obviousBindThreadIO ctx) $
110 L.find
111 ( ( \case
112 Just SingleBindMetrics{pPossibleDeadlock = True} -> False
113 Just SingleBindMetrics{pAlternative = 1} -> True
114 _ -> False
115 )
116 . cast
117 . sDecision
118 )
119 subForest
120
121 allBindsAndRefsIO :: SynthesisMethodConstraints tag v x t => BackendCtx tag v x t -> SynthesisMethod tag v x t
122 allBindsAndRefsIO ctx tree = do
123 subForest <-
124 filter ((\d -> isSingleBind d || isRefactor d) . sDecision)
125 <$> positiveSubForestIO ctx tree
126 case subForest of
127 [] -> return tree
128 _ -> allBindsAndRefsIO ctx $ minimumOn (defScore . sDecision) subForest
129
130 refactorThreadIO :: SynthesisMethodConstraints tag v x t => BackendCtx tag v x t -> SynthesisMethod tag v x t
131 refactorThreadIO ctx tree = do
132 subForest <- positiveSubForestIO ctx tree
133 maybe (return tree) (refactorThreadIO ctx) $
134 L.find (isRefactor . sDecision) subForest
135
136 smartBindThreadIO :: SynthesisMethodConstraints tag v x t => BackendCtx tag v x t -> SynthesisMethod tag v x t
137 smartBindThreadIO ctx tree = do
138 subForest <-
139 filter ((\d -> isSingleBind d || isRefactor d) . sDecision)
140 <$> (positiveSubForestIO ctx =<< refactorThreadIO ctx tree)
141 case subForest of
142 [] -> return tree
143 _ -> smartBindThreadIO ctx $ maximumOn (defScore . sDecision) subForest
144
145 allBestThreadIO :: SynthesisMethodConstraints tag v x t => BackendCtx tag v x t -> Int -> SynthesisMethod tag v x t
146 allBestThreadIO ctx (0 :: Int) tree = bestThreadIO ctx stepLimit tree
147 allBestThreadIO ctx n tree = do
148 subForest <- positiveSubForestIO ctx tree
149 leafs <- mapM (allBestThreadIO ctx (n - 1)) subForest
150 return $ bestLeaf tree leafs
151
152 bestLeaf :: SynthesisMethodConstraints tag v x t => DefTree tag v x t -> [DefTree tag v x t] -> DefTree tag v x t
153 bestLeaf tree leafs =
154 let successLeafs = filter (\node -> isComplete node && isLeaf node) leafs
155 in case successLeafs of
156 [] -> headDef tree leafs
157 _ : _ ->
158 minimumOn
159 (\Tree{sState = SynthesisState{sTarget}} -> (processDuration sTarget, puSize sTarget))
160 successLeafs
161
162 topDownByScoreSynthesisIO :: SynthesisMethodConstraints tag v x t => Float -> Int -> Maybe Text -> BackendCtx tag v x t -> SynthesisMethod tag v x t
163 topDownByScoreSynthesisIO = topDownByScoreSynthesisIO' (H.empty :: H.MaxPrioHeap Float (DefTree tag v x t)) 0
164
165 topDownByScoreSynthesisIO' heap step depthCoeffBase limit scoreKey ctx currentNode = do
166 if step > limit
167 then do
168 infoM "NITTA.Synthesis" $ "topDownByScoreSynthesisIO - STEP LIMIT REACHED: " <> show (sID currentNode)
169 return currentNode
170 else do
171 -- currentNode should not be in the heap at this point, but all its children will be
172 subForest <- positiveSubForestIO ctx currentNode
173 let getNodeDepth node = (\(Sid sidParts) -> length sidParts) $ sID node
174 -- priority calculation should prefer nodes that are closer to the leafs
175 depthCoeff = depthCoeffBase ** fromIntegral (getNodeDepth currentNode)
176 getScore node = case scoreKey of
177 Nothing -> defScore . sDecision $ node
178 Just key -> scores (sDecision node) M.! key
179 getPriority node = depthCoeff * getScore node
180 -- heapWithSubforest = foldl (\acc child -> H.insert (getPriority child, child) acc) heap subForest
181 -- the version above (fold + insert) takes 1.7x more time than below (fromList + union)
182 subForestOnlyHeap = H.fromList [(getPriority child, child) | child <- subForest]
183 heapWithSubforest = H.union heap subForestOnlyHeap
184
185 case H.viewHead heapWithSubforest of
186 Nothing -> do
187 infoM "NITTA.Synthesis" $ "topDownByScoreSynthesisIO - TREE EXHAUSTED: " <> show (sID currentNode)
188 return currentNode
189 Just (_, nextBestScoreNode) -> do
190 if isComplete nextBestScoreNode
191 then do
192 infoM "NITTA.Synthesis" $ "topDownByScoreSynthesisIO - DONE: " <> show (sID nextBestScoreNode)
193 return nextBestScoreNode
194 else do
195 let prio = getPriority nextBestScoreNode
196 depth = getNodeDepth nextBestScoreNode
197 score = getScore nextBestScoreNode
198 -- the more steps we make, the more aggressively we drop nodes to find new ones
199 aggressiveness = 0.5 :: Float -- [0.0; +inf)
200 maxDrops = 5
201 aggressiveDropPerSteps = 2500.0
202 aggressiveDropCount = min (maxDrops - 1) $ fromIntegral step / aggressiveDropPerSteps * aggressiveness
203 dropCount = round $ 1 + aggressiveDropCount * aggressiveness
204
205 infoM
206 "NITTA.Synthesis"
207 ( printf
208 "topDownByScoreSynthesisIO: prio=%-15s depth=%-5s score=%-10s drops=%-3s %s -> %s"
209 (show prio)
210 (show depth)
211 (show score)
212 (show dropCount)
213 (show $ sID currentNode)
214 (show $ sID nextBestScoreNode)
215 )
216
217 topDownByScoreSynthesisIO' (H.drop dropCount heapWithSubforest) (step + 1) depthCoeffBase limit scoreKey ctx nextBestScoreNode
218
219 -- * Helpers
220
221 selectSubForestIO ::
222 ( SynthesisMethodConstraints tag v x t
223 , m ~ TargetSystem (BusNetwork tag v x t) tag v x t
224 , ctx ~ SynthesisState m tag v x t
225 ) =>
226 (SynthesisDecision ctx m -> Bool) ->
227 BackendCtx tag v x t ->
228 DefTree tag v x t ->
229 IO [DefTree tag v x t]
230 selectSubForestIO p ctx tree = filter (p . sDecision) <$> positiveSubForestIO ctx tree
231
232 bestDecision :: [DefTree tag v x t] -> Maybe (DefTree tag v x t)
233 bestDecision [] = Nothing
234 bestDecision xs = Just $ maximumOn (defScore . sDecision) xs