scheduling.hs

Cores are generated from Confluence a modern logic design language. Confluence is a simple, yet high

-- | Atom rule scheduling.

module Language.Atom.Scheduling ( schedule ) where

import Control.Monad
import qualified Data.List as List
import Data.Maybe
import qualified Data.Set as Set
import System.IO

import Language.Atom.Elaboration
import Language.Atom.FeedbackArcSet
import qualified Language.Atom.SAT as SAT
import Language.Atom.Terms
import Language.Atom.Utils

-- | Schedules the 'Rule's of a 'SystemDB' and returns the enabling and data control for each 'Reg' and each display.
schedule :: String -> SystemDB -> [[String]] -> IO (Maybe RTL)
schedule name sys' priorities = do
  let sys = foldl insertLinearPriorities sys' priorities
  putStrLn "Starting rule scheduling optimization..."
  hFlush stdout
  results <- optimizePriority name $ initialSchedule $ sysRules sys
  case results of
    Nothing -> return Nothing
    Just (schedule, doc) -> do
      return $ Just RTL
        { rtlName = name
        , rtlSystem = sys
        , rtlDoc = doc
        , rtlAssigns = ruleLogic schedule (sysVars sys)
        }

type Schedule = [(Rule,[Rule])]

-- | Rule scheduling (priority) optimization.
optimizePriority :: String -> Schedule -> IO (Maybe (Schedule, String))
optimizePriority name rules = do
  --reducedEdges <- reduceEdges $ Set.unions [softEdges, priorityEdges, activeWhenEnabledEdges]
  reducedEdges <- reduceEdges $ Set.unions [softEdges, activeWhenEnabledEdges]
  --ruleOrder <- optimize (Set.fromList $ map fst rules) reducedEdges
  ruleOrder <- optimize name (Set.fromList $ map fst rules) $ Set.unions [reducedEdges, priorityEdges]
  case ruleOrder of
    Left rules  -> do
      putStrLn "ERROR: Following rules form a circular constraint:"
      mapM_ (\ rule -> putStrLn $ "  " ++ show rule) $ Set.toList rules
      return Nothing
    Right (rules, doc) -> return $ Just (map (groupDownstreams reducedEdges) rules, doc)
  where
  groupDownstreams :: Set.Set (Edge Rule) -> Rule -> (Rule,[Rule])
  groupDownstreams edges r = (r, mapMaybe f $ Set.toList edges)
    where
    f (Hard _ _)          = Nothing
    f (Soft a b) | r == a = Just b
    f (Soft _ _)          = Nothing

  ruleRelations' :: [(Rule,Relation)]
  ruleRelations' = concatMap (\ (r,_) -> zip (repeat r) (ruleRelations r)) rules

  softEdges :: Set.Set (Edge Rule)
  softEdges = Set.fromList $ concatMap (\ (from,rs) -> map (\ to -> Soft from to) rs) rules

  priorityEdges :: Set.Set (Edge Rule)
  priorityEdges = Set.fromList $ f ruleRelations'
    where
    f :: [(Rule,Relation)] -> [Edge Rule]
    f [] = []
    f ((rule, relation):relations) = case relation of
      Higher i -> map (\ r -> Hard rule r) (fst $ unzip $ filter (\ (_,rel) -> rel == Lower  i) relations) ++ f relations
      Lower  i -> map (\ r -> Hard r rule) (fst $ unzip $ filter (\ (_,rel) -> rel == Higher i) relations) ++ f relations

  activeWhenEnabledEdges :: Set.Set (Edge Rule)
  activeWhenEnabledEdges = Set.fromList $ concatMap f rules
    where
    f :: (Rule,[Rule]) -> [Edge Rule]
    f (r,_) = if ruleActiveWhenEnabled r then mapMaybe f' $ Set.toList softEdges else []
      where
      f' :: Edge Rule -> Maybe (Edge Rule)
      f' (Soft a b) | a == r = Just (Hard r b)
      f' _ = Nothing

-- | Builds the rule activation and data selection logic.
ruleLogic :: Schedule -> [UVar] -> [(UVar, UTerm)]
ruleLogic schedule vars = foldl selectionLogic defaults actives
  where
  actives = activationLogic schedule []
  defaults = map f vars
  f :: UVar -> (UVar, UTerm)
  f uv = case uv of
    UVarBool   v -> (uv, UTermBool    (value v))
    UVarInt    v -> (uv, UTermInt     (value v))
    UVarFloat  v -> (uv, UTermFloat   (value v))
    UVarDouble v -> (uv, UTermDouble  (value v))

-- | Builds the activation logic for all rules of a given 'Schedule'.
--   Returned list has low to high priority; reversed of 'Schedule'.
activationLogic :: Schedule -> [(Rule, Term Bool)] -> [(Rule, Term Bool)]
activationLogic [] actives  = actives
activationLogic ((rule, rulesDownstream) : rulesLowerPriority) higherPriorityActives = activationLogic rulesLowerPriority $ (rule, active) : higherPriorityActives
  where
  active = foldl andNot (ruleEnable rule) $ mapMaybe (flip lookup higherPriorityActives) rulesDownstream
  andNot a b = a &&. inv b

-- | Builds the data selection logic a rule.
selectionLogic :: [(UVar, UTerm)] -> (Rule, Term Bool) -> [(UVar, UTerm)]
selectionLogic vars (rule, active) = foldl updateVars vars $ ruleAssigns rule
  where
  updateVars :: [(UVar, UTerm)] -> (UVar, UTerm) -> [(UVar, UTerm)]
  updateVars assigns (uvar, uterm) = replace (uvar, uterm') assigns
    where
    uterm' = case (uterm, fromJust $ lookup uvar assigns) of
      (UTermBool   t1, UTermBool   t2) -> UTermBool   $ mux active t1 t2
      (UTermInt    t1, UTermInt    t2) -> UTermInt    $ mux active t1 t2
      (UTermFloat  t1, UTermFloat  t2) -> UTermFloat  $ mux active t1 t2
      (UTermDouble t1, UTermDouble t2) -> UTermDouble $ mux active t1 t2
      _ -> error "Schedule.updateVars"

  -- Replaces an element in an association list.
  replace :: Eq a => (a,b) -> [(a,b)] -> [(a,b)]
  replace (a,b) [] = [(a,b)]
  replace (a,b) ((a',_):c) | a == a' = (a,b):c
  replace (a,b) (h:c)                = h : replace (a,b) c


-- | Inserts linear rule priorities.
insertLinearPriorities :: SystemDB -> [String] -> SystemDB
insertLinearPriorities sys names = sys
  { sysNextId = sysNextId sys + length selectedRules - 1
  , sysRules = modifiedRules
  }
  where
  modifiedRules = insert (sysNextId sys) selectedRules ++ filter (flip notElem selectedRules) allRules
  selectedRules = mapMaybe (lookup allRules) names
  allRules = sysRules sys
  lookup :: [Rule] -> String -> Maybe Rule
  lookup [] _ = Nothing
  lookup (a:_) name | ruleName a == split name "." = Just a
  lookup (_:b) name = lookup b name
  insert :: Int -> [Rule] -> [Rule]
  insert _ [] = []
  insert _ [a] = [a]
  insert id (a:b:c) = a  { ruleRelations = Higher id : relationsA } :
                      b' { ruleRelations = Lower  id : relationsB } : c'
    where
    (b':c') = insert (id+1) (b:c)
    relationsA = ruleRelations a
    relationsB = ruleRelations b'


-- | Creates the initial rule priority 'Schedule'.
initialSchedule :: [Rule] -> Schedule
initialSchedule rules = map downstreamRules rules
  where

  downstreamRules :: Rule -> (Rule,[Rule])
  downstreamRules rule = (rule, mapMaybe isDownstreamRule upstreamRules)
    where
    isDownstreamRule :: ([Rule],Rule) -> Maybe Rule
    isDownstreamRule (rules, r) = if elem rule rules then Just r else Nothing

  upstreamRules :: [([Rule],Rule)]
  upstreamRules = map upstreamRulesOfRule rules

  upstreamRulesOfRule :: Rule -> ([Rule],Rule)
  upstreamRulesOfRule rule = (upstreamRules, rule)
    where
    upstreamRules = filter isUpstreamRule rules
    isUpstreamRule :: Rule -> Bool
    isUpstreamRule r | r == rule = False
    isUpstreamRule r = not $ Set.null $ Set.intersection uvarsAssigned upstreamUVars
      where
      uvarsAssigned = Set.fromList $ fst $ unzip $ ruleAssigns r

    upstreamUVars :: Set.Set UVar
    upstreamUVars = Set.union (termVars (ruleEnable rule)) $ Set.unions $ map uvarsInAssign $ ruleAssigns rule

    uvarsInAssign :: (UVar, UTerm) -> Set.Set UVar
    uvarsInAssign (_, uterm) = case uterm of
      UTermBool   t -> termVars t
      UTermInt    t -> termVars t
      UTermFloat  t -> termVars t
      UTermDouble t -> termVars t

-- | Reduces number of 'Edge's in a graph by using SAT to search for mutually excusive rules.
reduceEdges :: Set.Set (Edge Rule) -> IO (Set.Set (Edge Rule))
reduceEdges edges = do
  putStrLn "Starting rule mutual exclusion analysis..."
  hFlush stdout
  inclusiveRules <- filterM compareRules $ Set.toList ruleRelations
  return $ Set.filter (realEdge $ Set.fromList inclusiveRules) edges
  where
  ruleRelations :: Set.Set (Rule,Rule)
  ruleRelations = Set.fold insertEdge Set.empty edges
  insertEdge :: Edge Rule -> Set.Set (Rule,Rule) -> Set.Set (Rule,Rule)
  --insertEdge (Hard _ _) s = s
  insertEdge (Hard a b) s = Set.insert (min a b, max a b) s
  insertEdge (Soft a b) s = Set.insert (min a b, max a b) s
  compareRules :: (Rule,Rule) -> IO Bool
  compareRules (a,b) = do
    putStr $ "  checking eventually " ++ show a ++ " && " ++ show b ++ " => "
    hFlush stdout
    result <- mutuallyInclusive (ruleEnable a) (ruleEnable b)
    case result of
      Yes     -> putStrLn "yes"   >> hFlush stdout >> return True
      No      -> putStrLn "no"    >> hFlush stdout >> return False
      Unknown -> putStrLn "maybe" >> hFlush stdout >> return True
      
  realEdge :: Set.Set (Rule,Rule) -> Edge Rule -> Bool
  --realEdge _ (Hard _ _) = True
  realEdge s (Hard a b) = Set.member (min a b, max a b) s
  realEdge s (Soft a b) = Set.member (min a b, max a b) s

data YesNo = Yes | No | Unknown deriving Eq

-- | Mutual inclusive tests.  Checks if two rules could be enabled at the same time.
--   Assumes all rules could be enabled.
mutuallyInclusive :: Term Bool -> Term Bool -> IO YesNo
mutuallyInclusive (Const True) _ = return Yes
mutuallyInclusive _ (Const True) = return Yes
mutuallyInclusive a b = do
  case satSimple f of
    No -> return No
    _  -> if Set.null commonVars then return Yes else sat 20 f -- SAT with maxDepth.
  where
  commonVars = Set.intersection (termVars a) (termVars b)
  f = a &&. b

-- | SAT approximation.
satSimple :: Term Bool -> YesNo
satSimple f = if any (\ f -> Set.member (inv f) terms) $ Set.toList terms then No else Unknown
  where
  terms = conjunctiveLeaves f

conjunctiveLeaves :: Term Bool -> Set.Set (Term Bool)
conjunctiveLeaves f@(And a b) = Set.insert f $ Set.union (conjunctiveLeaves a) (conjunctiveLeaves b)
conjunctiveLeaves f = Set.singleton f

-- | Bounded SAT procedure.
sat :: Int -> Term Bool -> IO YesNo
sat maxDepth s = sat' 1 $ formula 0 s
  where
  sat' :: Int -> SAT.Formula (Term Bool) -> IO YesNo
  sat' i f = if f == f' then return Yes else if i > maxDepth then return Unknown else do
    result <- SAT.sat f'
    case result of
      Nothing -> return No
      Just _  -> sat' (i+1) f'
    where
    f' = formula i s

formula :: Int -> Term Bool -> SAT.Formula (Term Bool)
formula d s | d <= 0 = SAT.Var s
formula d s = case s of
  Inv a     -> SAT.Not (formula  d    a)
  And a b   -> SAT.And (formula (d-1) a) (formula (d-1) b)
  Const v   -> SAT.Const v
  Mux a b c -> formula d $ a &&. b ||. inv a &&. c
  s         -> SAT.Var s