{-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-undecidable-instances #-} {- Statically tracking `ticks' A `tick' may be an operation to read a byte from a hardware register, or to write such a byte. A computation may read a byte and chose a subcomputation depending on the value of that byte. These sub-computations may read further bytes. It is important that any sequence of sub-computations within one processing cycle has read the same number of bytes, so the protocol is obeyed and a frame is fully consumed. We should get this guarantee statically. Of course one may say we should read all bytes in a buffer... But: that requires a memory buffer, and a double-scan of data (first read and write into the buffer, then read from the buffer). The embedded device (for which we generate the code for, via code- generating combinators) may be under-powered for such buffering. The second application is to permit different paths through the code within one processing cycle differ in the number of ticks. But we want to accumulate the max number of ticks. So we can statically determine the worst `time complexity' of the code. When we generate the code, we may as well associate a number of ticks with a generated instruction (and hence, with its generator). So, we can statically estimate the worst-case time complexity and determine if our computation might fit within allocated time budget. Loops are no problem: all iterations in embedded systems must be bound in the number of steps. We can use IntBounded for representing the loop counter, and so estimate the max latency of a loop. -} module RealTime where import BinaryNumber import Areas (Ix, (<<=), toIxN, Succ, ixPred) import Prelude hiding (succ, max) -- Introduction. -- This code is based on tagging (monadic) computation with ticks. -- We need a simple variable-state monad (transformer) -- The following is excerpted from a message posted on the Haskell -- mailing list on Dec 17, 2006. -- However, our implementation here is different: the `state' is emphemeral -- (type-level only). That at the run-time, our state-changing `monad' -- is the same as the underlying, base monad. class Monadish m where gret :: a -> m p p a gbind :: m p q a -> (a -> m q r b) -> m p r b -- Inject regular monads to be monadish things too newtype MW m p q a = MW{ unMW:: m a } instance Monad m => Monadish (MW m) where gret = MW . return gbind (MW m) f = MW (m >>= unMW . f) -- Introduce the variable-type phantom state. It is operationally -- indistinguishable from the base monad m. newtype VST m si so v = VST{runVST:: m v} -- lift into the VST monad glift :: Monad m => m v -> VST m si si v glift = VST -- Pure type-level computation (attribution) vsputL :: Monad m => m v -> si -> so -> VST m si so v vsputL m _ _ = VST m instance Monad m => Monadish (VST m) where gret = VST . return gbind (VST m) f = VST (m >>= runVST . f) vsget :: forall m si. Monad m => VST m si si si vsget = VST (return (undefined::si)) vsput :: Monad m => so -> VST m si so () vsput x = VST (return ()) -- some syntactic sugar infixl 1 +>> vm1 +>> vm2 = gbind vm1 (const vm2) infixl 1 >== m >== f = gbind m f -- The first example: balanced ticks across the branches -- Our state is the number of ticks. Define the command that increments -- the tick -- tickL m = vsget >== vsput . succ +>> glift m -- The following is the same as above. However, it makes it clear -- there are no run-time computations. tickL :: (Monad m, Succ si so) => m v -> VST m si so v tickL = VST -- Define the command that `reads a byte'. We tag this command as -- `tickable', that is, advancing the tick counter tread_byte :: Succ si so => VST IO si so Int tread_byte = tickL (do putStrLn "Read byte" return 1) -- the value of the read byte -- Sample computation: -- We read a byte. We branch upon the byte value. In one branch, we -- read the second byte and branch again. In some branches, we have -- to add dummy reads to balance the reading in other branches. If -- we miss those, the compiler complaints. -- A do notation for `monadish' would have been nice. -- It was quite difficult to balance those things... tex1 = tread_byte >== \b1 -> if b1 > 10 then branch1 b1 else branch2 b1 +>> tread_byte +>> tread_byte where branch1 b = tread_byte >== \b2 -> if b2 > 10 then branch4 b2 +>> branch2 b2 else branch3 b2 branch2 b = tread_byte +>> tread_byte branch3 b = tread_byte +>> glift (putStrLn "branch3") +>> tread_byte +>> tread_byte branch4 b = tread_byte runst :: forall m so v. Monad m => VST m N0 so v -> m (so,v) runst m = runVST m >>= return . (,) (undefined::so) rundy m = runst m >>= ( \ (so,r) -> putStrLn $ "ticks " ++ show (toInt so) ++ " result: " ++ show r) te1 = runst tex1 {- It takes 5 ticks. The compiler has figured that out *RealTime> :t te1 te1 :: IO (U (U B1 B0) B1, Int) -} te2 = rundy tex1 -- The second example: worst-case complexity -- Needed a new branching combinator data Else = Else gif tst th Else el = vsputL (if tst then runVST th else runVST el) si sm where (si1,st) = gets th -- these aren't actually run! (si2,se) = gets el sm = max st se si = if True then si1 else si2 gets :: VST m si so v -> (si,so); gets = undefined -- now, branches are not balanced tex2 () = tread_byte >== ( \b1 -> gif (b1 > 10) (branch1 b1) Else (branch2 b1 +>> tread_byte +>> tread_byte)) where branch1 b = tread_byte >== (\b2 -> gif (b2 > 10) (branch4 b2 +>> branch2 b2) Else (branch3 b2)) branch2 b = tread_byte +>> tread_byte branch3 b = glift (putStrLn "branch3") +>> tread_byte branch4 b = tread_byte +>> tread_byte te3 = runst (tex2 ()) {- The worst-case complexity through the branches *RealTime> :t te3 te3 :: IO (U (U B1 B1) B0, Int) -} te4 = rundy (tex2 ()) -- The third example: worst-case complexity in the presence of loops -- First, we read a byte from the register. If it is less than 10, -- we read that many more bytes. Otherwise, we just read one more -- byte. Compute the worst-time complexity. nat10 = add nat2 nat8 -- type-level numerals tex3 () = tread_byte >== \b1 -> gmaybe (branch2 b1) (loop b1) (toIxN nat10 b1) where branch2 _ = tread_byte loop b ix = foldTM branch1 b ix branch1 b = glift (putStrLn "branch1") +>> tread_byte +>> tread_byte -- FoldM with an upper-bound tick accumulation. That code should be -- in the security kernel. foldTM :: (Monad m, NatE n, Succ n' n, Add si diff so', Mul diff n' grand_diff, Add si grand_diff so) => (v -> VST m si so' v) -> v -> Ix n -> VST m si so v foldTM f seed ix = VST( loop seed (ixPred ix) ) where loop seed ixm = maybe (return seed) (loop' seed) ((minBound `asTypeOf` ix) <<= ixm) loop' seed ix = do seed' <- runVST (f seed); loop seed' (ixPred ix) gmaybe onnothing onjust mv = vsputL (maybe (runVST onnothing) (runVST . onjust) mv) si sm where (si1,st) = gets onnothing -- these aren't actually run! (si2,se) = gets (onjust undefined) sm = max st se si = if True then si1 else si2 gets :: VST m si so v -> (si,so); gets = undefined te5 = runst (tex3 ()) {- The worst-case complexity through the branches *RealTime> :t te5 te5 :: IO (U (U (U B1 B0) B1) B0, Int) -} te7 = rundy (tex3 ())