atom 0.1.2 → 0.1.3

raw patch · 9 files changed

+121/−61 lines, 9 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• Language/Atom/Code.hs +29/−21
• Language/Atom/Common.hs +8/−0
• Language/Atom/Compile.hs +1/−1
• Language/Atom/Elaboration.hs +48/−27
• Language/Atom/Language.hs +8/−4
• Language/Atom/Scheduling.hs +2/−1
• Language/Atom/Unit.hs +8/−2
• RELEASE-NOTES +6/−0
• atom.cabal +11/−5

@@ -28,9 +28,8 @@   , cType         :: Type -> String                                          -- ^ C type naming rules.   , cCode         :: [Name] -> [Name] -> [(Name, Type)] -> (String, String)  -- ^ Custom C code to insert above and below, given assertion names, coverage names, and probe names and types.   , cRuleCoverage :: Bool                                                    -- ^ Enable rule coverage tracking.-  , cAssert       :: Bool                                                    -- ^ Enable assertion checking.+  , cAssert       :: Bool                                                    -- ^ Enable assertions and functional coverage.   , cAssertName   :: String                                                  -- ^ Name of assertion function.  Type: void assert(int, cType Bool, cType Word64);-  , cCover        :: Bool                                                    -- ^ Enable functional coverage accumulation.   , cCoverName    :: String                                                  -- ^ Name of coverage function.  Type: void cover(int, cType Bool, cType Word64);   } @@ -43,7 +42,6 @@   , cRuleCoverage = True   , cAssert       = True   , cAssertName   = "assert"-  , cCover        = True   , cCoverName    = "cover"   } @@ -129,10 +127,10 @@  type RuleCoverage = [(Name, Int, Int)] -writeC :: Name -> Config -> Schedule -> [UV] -> [UA] -> [Name] -> [Name] -> [(Name, Type)] -> IO RuleCoverage-writeC name config schedule uvs uas assertionNames coverageNames probeNames = do+writeC :: Name -> Config -> [Rule] -> Schedule -> [UV] -> [UA] -> [Name] -> [Name] -> [(Name, Type)] -> IO RuleCoverage+writeC name config rules schedule uvs uas assertionNames coverageNames probeNames = do   writeFile (name ++ ".c") c-  return [ (ruleName r, div (ruleId r) 32, mod (ruleId r) 32) | r <- rules ]+  return [ (ruleName r, div (ruleId r) 32, mod (ruleId r) 32) | r <- rules' ]   where   (preCode, postCode) = cCode config assertionNames coverageNames probeNames   c = unlines@@ -144,7 +142,8 @@     , codeIf (cRuleCoverage config) $ "static " ++ cType config Word32 ++ " __coverage_index = 0;"     , concatMap (declUV config) uvs     , concatMap (declUA config) uas-    , concatMap (codeRule config assertionNames coverageNames) $ rules+    , concatMap (codeRule config) rules'+    , codeAssertionChecks config assertionNames coverageNames rules     , "void " ++ (if null (cFuncName config) then name else cFuncName config) ++ "(void) {"     , concatMap (codePeriodPhase config) schedule     , "  __global_clock = __global_clock + 1;"@@ -153,10 +152,10 @@     , postCode     ] -  rules :: [Rule]-  rules = concat [ r | (_, _, r) <- schedule ]+  rules' :: [Rule]+  rules' = concat [ r | (_, _, r) <- schedule ] -  covLen = 1 + div (maximum $ map ruleId rules) 32+  covLen = 1 + div (maximum $ map ruleId rules') 32  codeIf :: Bool -> String -> String codeIf a b = if a then b else ""@@ -191,16 +190,14 @@ doubleBits :: Double -> Word64 doubleBits = unsafeCoerce -codeRule :: Config -> [Name] -> [Name] -> Rule -> String-codeRule config assertionNames coverageNames rule =+codeRule :: Config -> Rule -> String+codeRule config rule@(Rule _ _ _ _ _ _ _) =   "/* " ++ show rule ++ " */\n" ++   "static void __r" ++ show (ruleId rule) ++ "(void) {\n" ++   concatMap (codeUE    config ues "  ") ues ++   "  if (" ++ id (ruleEnable rule) ++ ") {\n" ++   concatMap codeAction (ruleActions rule) ++   codeIf (cRuleCoverage config) ("    __coverage[" ++ covWord ++ "] = __coverage[" ++ covWord ++ "] | (1 << " ++ covBit ++ ");\n") ++-  concat [ codeIf (cAssert config) ("    " ++ cAssertName config ++ "(" ++ assertionId name ++ ", " ++ id check ++ ", __global_clock);\n") | (name, check) <- ruleAsserts rule ] ++-  concat [ codeIf (cCover  config) ("    " ++ cCoverName  config ++ "(" ++ coverageId  name ++ ", " ++ id check ++ ", __global_clock);\n") | (name, check) <- ruleCovers  rule ] ++   "  }\n" ++   concatMap codeAssign (ruleAssigns rule) ++   "}\n\n"@@ -208,12 +205,6 @@   ues = topo $ allUEs rule   id ue = fromJust $ lookup ue ues -  assertionId :: Name -> String-  assertionId name = show $ fromJust $ elemIndex name assertionNames--  coverageId :: Name -> String-  coverageId name = show $ fromJust $ elemIndex name coverageNames-   codeAction :: (([String] -> String), [UE]) -> String   codeAction (f, args) = "    " ++ f (map id args) ++ ";\n" @@ -229,6 +220,23 @@       UVArray (UAExtern n _) index -> concat [n, "[", id index, "]"]       UVExtern n _                 -> n +codeRule _ _ = ""++codeAssertionChecks :: Config -> [Name] -> [Name] -> [Rule] -> String+codeAssertionChecks config assertionNames coverageNames rules = codeIf (cAssert config) $+  "static void __assertion_checks(void) {\n" +++  concatMap (codeUE config ues "  ") ues +++  concat [ "  if (" ++ id enable ++ ") " ++ cAssertName config ++ "(" ++ assertionId name ++ ", " ++ id check ++ ", __global_clock);\n" | Assert name enable check <- rules ] +++  concat [ "  if (" ++ id enable ++ ") " ++ cCoverName  config ++ "(" ++ coverageId  name ++ ", " ++ id check ++ ", __global_clock);\n" | Cover  name enable check <- rules ] +++  "}\n\n"+  where+  ues = topo $ concat [ [a, b] | Assert _ a b <- rules ] ++ concat [ [a, b] | Cover _ a b <- rules ]+  id ue = fromJust $ lookup ue ues+  assertionId :: Name -> String+  assertionId name = show $ fromJust $ elemIndex name assertionNames+  coverageId :: Name -> String+  coverageId name = show $ fromJust $ elemIndex name coverageNames+ codePeriodPhase :: Config -> (Int, Int, [Rule]) -> String codePeriodPhase config (period, phase, rules) = unlines   [ printf "  {"@@ -246,5 +254,5 @@   clockType | period < 2 ^  8 = Word8             | period < 2 ^ 16 = Word16             | otherwise       = Word32-  callRule r = concat ["      __r", show (ruleId r), "();  /* ", show r, " */"]+  callRule r = concat ["      ", codeIf (cAssert config) "__assertion_checks(); ", "__r", show (ruleId r), "();  /* ", show r, " */"] 

@@ -14,6 +14,7 @@   , debounce   -- * Lookup Tables   , lookupTable+  , linear   -- * Hysteresis   , hysteresis   ) where@@ -87,6 +88,13 @@     slope = (y1 - y0) / (x1 - x0)     interp = (x - x0) * slope + y0 +-- | Linear extrapolation and interpolation on a line with 2 points.+--   The two x points must be different to prevent a divide-by-zero.+linear :: FloatingE a => (E a, E a) -> (E a, E a) -> E a -> E a+linear (x1, y1) (x2, y2) a = slope * a + inter+  where+  slope = y2 - y1 / x2 - x1+  inter = y1 - slope * x1  -- | Hysteresis returns 'True' when the input exceeds @max@ and 'False' when --   the input is less than @min@.  The state is held when the input is between

@@ -23,6 +23,6 @@     Nothing -> putStrLn "ERROR: Design rule checks failed." >> exitWith (ExitFailure 1)     Just (rules, uvs, uas, assertionNames, coverageNames, probeNames) -> do       let schedule' = schedule rules-      ruleCoverage <- writeC name config schedule' uvs uas assertionNames coverageNames probeNames+      ruleCoverage <- writeC name config rules schedule' uvs uas assertionNames coverageNames probeNames       return (schedule', ruleCoverage, assertionNames, coverageNames, probeNames) 

@@ -63,29 +63,36 @@   , atomCovers      :: [(Name, UE)]   } -data Rule = Rule-  { ruleId        :: Int-  , ruleName      :: Name-  , ruleEnable    :: UE-  , ruleAssigns   :: [(UV, UE)]-  , ruleActions   :: [([String] -> String, [UE])]-  , rulePeriod    :: Int-  , rulePhase     :: Int-  , ruleAsserts   :: [(Name, UE)]-  , ruleCovers    :: [(Name, UE)]-  }+data Rule+  = Rule+    { ruleId        :: Int+    , ruleName      :: Name+    , ruleEnable    :: UE+    , ruleAssigns   :: [(UV, UE)]+    , ruleActions   :: [([String] -> String, [UE])]+    , rulePeriod    :: Int+    , rulePhase     :: Int+    }+  | Assert+    { ruleName      :: Name+    , ruleEnable    :: UE+    , ruleAssert    :: UE+    }+  | Cover+    { ruleName      :: Name+    , ruleEnable    :: UE+    , ruleCover     :: UE+    }  instance Show AtomDB where show = atomName instance Eq   AtomDB where (==) = (==) `on` atomId instance Ord  AtomDB where compare a b = compare (atomId a) (atomId b) instance Show Rule   where show = ruleName-instance Eq   Rule   where (==) = (==) `on` ruleId-instance Ord  Rule   where compare a b = compare (ruleId a) (ruleId b)  elaborateRules:: UE -> AtomDB -> [Rule] elaborateRules parentEnable atom = if isRule then rule : rules else rules   where-  isRule = not $ null (atomAssigns atom) && null (atomActions atom) && null (atomAsserts atom) && null (atomCovers atom)+  isRule = not $ null (atomAssigns atom) && null (atomActions atom)   enable = uand parentEnable $ atomEnable atom   rule = Rule     { ruleId        = atomId   atom@@ -95,17 +102,26 @@     , ruleActions   = atomActions atom     , rulePeriod    = atomPeriod  atom     , rulePhase     = atomPhase   atom-    , ruleAsserts   = atomAsserts atom-    , ruleCovers    = atomCovers  atom     }-  rules = concatMap (elaborateRules enable) (atomSubs atom)+  assert (name, ue) = Assert+    { ruleName      = name+    , ruleEnable    = enable+    , ruleAssert    = ue+    }+  cover (name, ue) = Cover+    { ruleName      = name+    , ruleEnable    = enable+    , ruleCover     = ue+    }+  rules = map assert (atomAsserts atom) ++ map cover (atomCovers atom) ++ concatMap (elaborateRules enable) (atomSubs atom)   enableAssign :: (UV, UE) -> (UV, UE)   enableAssign (uv, ue) = (uv, umux enable ue $ UVRef uv) -reIdRules :: [Rule] -> [Rule]-reIdRules rules = map (\ r -> r { ruleId = fromJust $ lookup (ruleId r) ids } ) rules-  where-  ids = zip (map ruleId rules) [0..]+reIdRules :: Int -> [Rule] -> [Rule]+reIdRules _ [] = []+reIdRules i (a:b) = case a of+  Rule _ _ _ _ _ _ _ -> a { ruleId = i } : reIdRules (i + 1) b+  _                  -> a                : reIdRules  i      b  buildAtom :: Global -> Name -> Atom a -> IO (a, (Global, AtomDB)) buildAtom g name (Atom f) = f (g { gRuleId = gRuleId g + 1 }, AtomDB@@ -154,9 +170,9 @@ elaborate :: Name -> Atom () -> IO (Maybe ([Rule], [UV], [UA], [Name], [Name], [(Name, Type)])) elaborate name atom = do   (_, (g, atomDB)) <- buildAtom Global { gRuleId = 0, gVarId = 0, gArrayId = 0, gVars = [], gArrays = [], gProbes = [], gPeriod = 1, gPhase  = 0 } name atom-  let rules = reIdRules $ elaborateRules (ubool True) atomDB-      coverageNames  = concatMap (fst . unzip . ruleCovers ) rules-      assertionNames = concatMap (fst . unzip . ruleAsserts) rules+  let rules = reIdRules 0 $ elaborateRules (ubool True) atomDB+      coverageNames  = [ name | Cover  name _ _ <- rules ]+      assertionNames = [ name | Assert name _ _ <- rules ]       probeNames = [ (n, typeOf a) | (n, a) <- gProbes g ]   if (null rules)     then do@@ -177,7 +193,7 @@  -- | Check that a variable is assigned more than once in a rule.  Will eventually be replaced consistent assignment checking. checkAssignConflicts :: Rule -> IO Bool-checkAssignConflicts rule =+checkAssignConflicts rule@(Rule _ _ _ _ _ _ _) =   if length vars /= length vars'     then do       putStrLn $ "ERROR: Rule " ++ show rule ++ " contains multiple assignments to the same variable(s)."@@ -187,6 +203,7 @@   where   vars = fst $ unzip $ ruleAssigns rule   vars' = nub vars+checkAssignConflicts _ = return True  {- -- | Checks that all array indices are not a function of array variables.@@ -280,7 +297,7 @@ allUVs :: [Rule] -> UE -> [UV] allUVs rules ue = fixedpoint next $ nearestUVs ue   where-  assigns = concatMap ruleAssigns rules+  assigns = concat [ ruleAssigns r | r@(Rule _ _ _ _ _ _ _) <- rules ]   previousUVs :: UV -> [UV]   previousUVs uv = concat [ nearestUVs ue | (uv', ue) <- assigns, uv == uv' ]   next :: [UV] -> [UV]@@ -292,9 +309,13 @@  -- | All primary expressions used in a rule. allUEs :: Rule -> [UE]-allUEs rule = ruleEnable rule : concat [ ue : index uv | (uv, ue) <- ruleAssigns rule ] ++ concat (snd (unzip (ruleActions rule))) ++ snd (unzip (ruleAsserts rule)) ++ snd (unzip (ruleCovers rule))+allUEs rule = ruleEnable rule : ues   where   index :: UV -> [UE]   index (UVArray _ ue) = [ue]   index _ = []+  ues = case rule of+    Rule _ _ _ _ _ _ _ -> concat [ ue : index uv | (uv, ue) <- ruleAssigns rule ] ++ concat (snd (unzip (ruleActions rule)))+    Assert _ _ a       -> [a]+    Cover  _ _ a       -> [a] 

@@ -287,7 +287,9 @@   return (value $ V $ UVExtern "__coverage_index" Word32, value $ V $ UVExtern "__coverage[__coverage_index]" Word32)  --- | Assertion that checks an E Bool.  Assertions are only checked if the containing rule is enabled and executed.+-- | An assertions checks that an E Bool is true.  Assertions are checked between the execution of every rule.+--   Parent enabling conditions can disable assertions, but period and phase constraints do not.+--   Assertion names should be globally unique. assert :: Name -> E Bool -> Atom () assert name check = do   (g, atom) <- get@@ -301,11 +303,13 @@   assert name $ imply a b   cover (name ++ "Precondition") a --- | Adds a functional coverage point.+-- | A functional coverage point tracks if an event has occured (true).+--   Coverage points are checked at the same time as assertions.+--   Coverage names should be globally unique. cover :: Name -> E Bool -> Atom () cover name check = do   (g, atom) <- get-  let names = fst $ unzip $ atomAsserts atom-  when (elem name names) (liftIO $ putStrLn $ "WARNING: Assertion name already used: " ++ name)+  let names = fst $ unzip $ atomCovers atom+  when (elem name names) (liftIO $ putStrLn $ "WARNING: Coverage name already used: " ++ name)   put (g, atom { atomCovers = (name, ue check) : atomCovers atom }) 

@@ -13,8 +13,9 @@ type Schedule = [(Int, Int, [Rule])]  -- (period, phase, rules)  schedule :: [Rule] -> Schedule-schedule rules = concatMap spread periods+schedule rules' = concatMap spread periods   where+  rules = [ r | r@(Rule _ _ _ _ _ _ _) <- rules' ]    -- Algorithm for assigning rules to phases for a given period: 

@@ -88,6 +88,8 @@ runTest :: Int -> IO Test -> IO (Name, Bool, Int, [Name], [Name]) runTest seed test = do   test <- test+  putStrLn $ "running test " ++ name test ++ " ..."+  hFlush stdout   (_, _, _, coverageNames, _) <- compile "atom_unit_test" defaults { cCode = prePostCode test, cRuleCoverage = False } $ testbench test   (exit, out, err) <- readProcessWithExitCode "gcc" (["-Wall", "-g", "-o", "atom_unit_test"] ++ [ "-i" ++ i | i <- includes test ] ++ modules test ++ ["atom_unit_test.c"]) ""   let file = name test ++ ".log"@@ -110,11 +112,15 @@       , "#include <stdlib.h>"       , "void assert (int id, unsigned char check, unsigned long long clock) {"       , "  static unsigned char failed[" ++ show (length assertionNames) ++ "] = {" ++ intercalate "," (replicate (length assertionNames) "0") ++ "};"-      , "  " ++ intercalate "\n  else " [ "if (id == " ++ show id ++ ") { if (! check && ! failed[id]) { printf(\"ASSERTION FAILURE: " ++ name ++ " at time %lli\\n\", clock); failed[id] = 1; } }" | (name, id) <- zip assertionNames [0..] ]+      , "  if (! check) {"+      , "    " ++ intercalate "\n    else " [ "if (id == " ++ show id ++ ") { if (! failed[id]) { printf(\"ASSERTION FAILURE: " ++ name ++ " at time %lli\\n\", clock); failed[id] = 1; } }" | (name, id) <- zip assertionNames [0..] ]+      , "  }"       , "}"       , "void cover  (int id, unsigned char check, unsigned long long clock) {"       , "  static unsigned char covered[" ++ show (length coverageNames) ++ "] = {" ++ intercalate "," (replicate (length coverageNames) "0") ++ "};"-      , "  " ++ intercalate "\n  else " [ "if (id == " ++ show id ++ ") { if (check && ! covered[id]) { printf(\"covered: " ++ name ++ " at time %lli\\n\", clock); covered[id] = 1; } }" | (name, id) <- zip coverageNames [0..] ]+      , "  if (check) {"+      , "    " ++ intercalate "\n    else " [ "if (id == " ++ show id ++ ") { if (! covered[id]) { printf(\"covered: " ++ name ++ " at time %lli\\n\", clock); covered[id] = 1; } }" | (name, id) <- zip coverageNames [0..] ]+      , "  }"       , "}"       ] ++ declCode test 

@@ -1,3 +1,9 @@+atom 0.1.3    12/03/2009++- Added linear lookup (Common). +- Assertions and coverage points are checked between the execution of every rule, not just once per cycle.+- Removed cCover code configuration.  Assertions and coverage are enabled by cAssert.+ atom 0.1.2    11/25/2009  - Added div0_ and mod0_ functions, that instrument runtime checks for divide-by-zero (Lee Pike).

@@ -1,15 +1,21 @@ name:    atom-version: 0.1.2+version: 0.1.3  category: Language  synopsis: A DSL for embedded hard realtime applications.  description:-    Atom is a Haskell DSL for designing hard realtime embedded programs. Based-    on conditional term rewriting, atom will compile a collection of atomic-    state transition rules to a C program with constant memory use and-    deterministic execution time.+    Atom is a Haskell DSL for designing hard realtime embedded software.+    Based on guarded atomic actions (similar to STM), Atom enables+    highly concurrent programming without the need for mutex locking.++    In addition, Atom performs compile-time task scheduling and generates code+    with deterministic execution time and constant memory use, simplifying the+    process of timing verification and memory consumption in hard realtime applications.++    Without mutex locking and run-time task scheduling, Atom eliminates+    the need and overhead of RTOSs for many embedded applications.  author:     Tom Hawkins <tomahawkins@gmail.com> maintainer: Tom Hawkins <tomahawkins@gmail.com>