{-# 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 ())