Re: Keeping local types local?

[oleg@okmij.org]

It seems the following section might be relevant to the present
discussion. It deals with a related problem: a function yield ()
should _not_ be invoked within the dynamic extent of the function
irq_disable. The latter takes a thunk and executes it with disabled
interrupts. This is a so-called yield problem in operating systems:

	Hao Chen and Jonathan S. Shapiro,
	Using Build-Integrated Static Checking to Preserve Correctness 
	Invariants, CCS2004, pp. 288--297
	http://www.eros-os.org/papers/ccs04.pdf

The problem is quite like the one we've discussed, up to the inverse:
you wish to enforce that set() and get() are only invoked within the
dynamic extent of the initialization function. The yield problem is to
prevent yield() from being invoked, within the specified dynamic extent.

The section below was present in an earlier draft of the regions IO
paper written with Chung-chieh Shan. The section discusses two other
OCaml solutions to the problem, which haven't been mentioned yet. The
yield.ml code discussed at the end is available here:

	http://okmij.org/ftp/Computation/resource-aware-prog/yield.ml

I should also point out the file yield.elf in the same directory. It
formally proves the safety of the monadic solution to the problem. The
safety is the corollary to the Progress theorem. The dynamic semantics
does not define the transition for yield() executed with any level of
disabled interrupts. Thus the evaluation of yield() in that context
gets stuck. The formally proven Progress theorem states that the
evaluation of the well-typed term does not get stuck.


Begin excerpt:
\subsection{Types versus effects}

This approach cannot be embedded in direct style in an impure language
such as OCaml to provide the same static safety guarantees. We can
easily define a higher-order function |irq_disable| that takes a thunk
as argument and executes it with interrupts disabled. However, using ML
facilities alone without external tools, we cannot statically prevent
invoking this function as 
\begin{code}
irq_disable (fun () -> yield (); ())
\end{code}
and thus executing |yield| with interrupts disabled.  This is because
the safe expression |()| and the unsafe one |(yield (); ())| have the same
type no matter what type we assign to |yield|. 

We need an effect system, such as \citearound{'s exception checker for
OCaml}\citet{leroy-type-based}. If the desired safety property were to
invoke |yield| only when interrupts are disabled (which is the opposite
of our problem), we could encode the property in terms of exceptions by
pretending that |yield| might raise an exception.
\begin{code}
let yield () = 
  if false then raise YieldExc else do_yield ()
\end{code}
The |irq_disable| function would then catch the exception.  Alas, our
problem is different, and the exception checker is external to OCaml.
An unappealing alternative is to abandon direct style and program
instead in continuation\hyp passing or monadic style, perhaps using some
syntactic sugar analogous to Haskell's |do| notation.  A third approach
is to use MetaOCaml to synthesize the interrupt handling code in direct
style, ensuring the yield property along the way.  Some microkernels
\citep{gabber-pebble} use this idea of run-time code generation, but it
is too static for our needs (see |yield.ml|).