{-# OPTIONS -fglasgow-exts #-}

-- Solving the `Yield Problem'
{-

The problem was posed in the paper
  Hao Chen and Jonathan S. Shapiro: Using build-integrated static 
  checking to preserve correctness invariants.
  CCS '04: Proceedings of the 11th ACM conference on computer and
  communications security, 2004, pp. 288--297.

They wrote: ``The program should not call Yield() when interrupts are
disabled. (Section 4.1 explains this property in details). The kernel
may enable an interrupt by calling irq_ENABLE() and disable an
interrupt by irq_DISABLE().  The MOPS user describes this property by
an FSA. Figure 1(a) shows this FSA, and Figure 1(b) shows a code
fragment that violates this property.''

It seems the problem is more general; for example, it can be
formulated as a `lock problem': every lock acquisition must be
balanced with the lock release. The program must not call a function
that may block while holding a lock. A lock cannot be acquired twice;
only acquired lock may released, and exactly once.

Chen and Shapiro elaborate: 
``The simplest property we attempted was ensuring that interrupt
enables and disables are properly bracketed. Every disable should be
balanced by a corresponding enable, and there should not be redundant
enables. In addition, the Yield() function (which abandons the current
system call) should not be called while interrupts are disabled. This
is because Yield() abandons the current kernel control flow and
invokes a kernel system call, but all kernel system calls are expected
to be invoked with interrupts enabled. The FSA in Figure 2 describes
this property.  A problem with checking interrupt enable and disable
is that it requires a stack or a counter. Finite state automata are
not powerful enough to implement counters,...''  

The more complex property corresponds to recursive locks: a process
holding a lock may acquire it again; each acquisition must be balanced
by the corresponding release.


In the code below, the function irq_disable implements the simple
policy, with no nested disabling. A trivial modification gives
nesting, with as many levels as needed. The latter cannot be achieved
with FSM-based approaches (as Chen and Shapiro point out themselves).

A more liberal property -- every lock must be released, but it is harmless
to release a lock that is not held -- corresponds to the type system 
for simple shift/reset.

Granted, the following code must be monadic (as one would expect since
we are dealing with the external world with locks, interrupts, etc).
Compare with SEL4: Derrin, Elphinstone, Klein, Cock, and Chakravarty:
Running the manual: An approach to high-assurance microkernel development.
Proc.  2006 Haskell workshop, pp. 60-71.
who also use monad in their implementation of SEL4 kernel prototype. The
House project also used a special (`hardware') monad throughout their kernel.

Joint work with Chung-chieh Shan.

$Id: yield.hs 2380 2007-06-15 05:34:07Z oleg $

-}

-- Design decisions: should the runM function be publicly available?
-- If yes, we need an extra polymorphic parameter, like 's' in runST,
-- to prevent the user doing something like 'lift $ runM yield' while within
-- the disabled block.
-- If runM is a part of security kernel, we don't need such a parameter:
-- cf IO vs ST s.
-- For now, we chose the simpler, IO-like way: runM is a part of the security
-- kernel.

-- This code is simple enough so that its safety can be verified
-- in Twelf!

module YieldProp where

import Control.Monad
import Control.Monad.Trans
import Data.IORef

test1 = runM $ -- runM is outside the programmers control
	 do
	 lputStrLn "test1"
	 yield
	 irq_disable (in_disabled (lputStrLn "passed action"))
	 -- expected type error
	 -- irq_disable (in_disabled (lputStrLn "passed action" >> yield))
	 yield
	 lputStrLn "done test1"

in_disabled m = do
		let a = lputStrLn "in disabled"
		a
		m -- execute the received action
		-- yield -- will cause the type error in test1
		return ()

test2 = runM $ -- runM is outside the programmers control
	 do
	 let aouter = lputStrLn "test2"
	 aouter
	 yield
	 ref <- liftIO $ newIORef undefined
	 irq_disable (do
		      let a = lputStrLn "in disabled"
		      a
		      -- liftIO $ writeIORef ref aouter
		      -- comment the line before and uncomment the one below
		      -- to test leaking of a
		      -- liftIO $ writeIORef ref a
		      liftIO $ writeIORef ref yield
		      return ()
		      )
	 a <- liftIO $ readIORef ref
	 a
	 lputStrLn "done test2"


-- recursive disabling: triple-nested disabling of interrupts,
-- all properly nested. yield may not be used while interrupts
-- are disabled at any level
test3 = runM $ -- runM is outside the programmers control
	 do
	 lputStrLn "test3"
	 yield
	 irq_disable (
		irq_disable
		  (in_disabled 
		     (irq_disable (lputStrLn "passed action"))))
	 -- expected type error
{-
	 irq_disable (
		irq_disable
		  (in_disabled 
		     (irq_disable yield)))
-}
	 -- expected type error
{-
	 irq_disable (
		irq_disable
		  (in_disabled 
		     (irq_disable (lputStrLn "passed action")))
		>> yield)
-}
	 yield
	 lputStrLn "done test3"

-- Labels:
data Enabled
data Disabled r

-- Security kernel

newtype M r a = M {unM :: IO a} -- unM and data constructor are NOT exported
    deriving (Monad, MonadIO)

-- The yield morphism
yield :: M Enabled ()
yield = lputStrLn "yielding"

-- we don't use bracket because we don't use Haskell exceptions.
-- Like in SEL4, Haskell exceptions are fatal...
irq_disable :: M (Disabled r) a -> M r a
irq_disable db = do
		 lputStrLn "Entering the disabled IRQ block"
		 res <- liftIO $ unM db
		 lputStrLn "re-enabling interrupts"
		 return res

-- runM is not exported! cf. `runIO'
runM :: M Enabled a -> IO a
runM = unM

lputStrLn s = liftIO $ putStrLn s