tps : eval E E' -> of E T -> of E' T -> type.
%mode tps +R +P -Q.
- : tps (eval1 PR PF) PTE (PF' _ PTR')
<- tpsfocus PF PTE PTR PF'
<- tpsrdx PR PTR PTR'.
%worlds () (tps D P _).
%total D (tps D P _).
and the key progress lemma, if a focusable expression has a type it can be reduced,
fprog : focus E PPV C -> of E T -> eval E E' -> type.
%mode fprog +F +P -D.
- : fprog (PF : focus E PPV _) PT (eval1 R PF)
<- tpsfocus PF PT PTPV _
<- typed-preval PPV PTPV R.
%worlds () (fprog _ _ _).
%total {} (fprog _ _ _).
share the same lemma tpsfocus -- asserting that if an expression is well-typed then the result of its focusing is well-typed. Evaluation contexts are modeled as meta-level functions.Andrew K. Wright and Matthias Felleisen. A Syntactic Approach to Type Soundness
Information and Computation, v115, N1, pp. 38-94, 1994
Our broad goal is designing a trusted kernel to statically assure safety of a (recursive, multi-level) critical section: the program may re-enter the critical section but must not execute any blocking operation until it fully exited the critical section. To prove that the trusted kernel enforces the yield property we extend our previous syntactic proof for empty-list and array-bound checking: We define a language Strict with a sound type system, then show that any well-typed program in Lax (an idealization of Haskell) that uses only the exported names from the trusted kernel is a translation of a well-typed Strict program.
Our language Strict extends System F with a family of monads mn, one for each natural number n (an interrupt level). To the standard expressions of System F we add do and ret and special operations disable and yield. The latter corresponds to a blocking operation; disable e executes e in a critical section with the interrupts disabled by one level.
The dynamic semantics of Strict is formulated in terms of two mutually recursive reduction functions. The simplification function reduces terms; it is the standard call-by-name reduction of System F terms. The execution function operates on configurations <n,e> where n is the interrupt level and e is a term (of a monadic type). This distinction between two reduction relations is characteristic of monadic metalanguages.
The execution of disable and yield changes and checks the interrupt level. Accordingly, these constructs call for the only typing rules not standard for System F and monads. Not coincidentally, it is these typing rules that assure the yield property. Our mechanized proof of type preservation and progress essentially verifies that the typing rules match the dynamic semantics for disable and yield.
Using Twelf, we demonstrate the fully worked-out formal semantics of Strict and the complete formal proofs of type preservation and progress. Since we have two evaluation relations -- simplification and execution, corresponding to the two levels of the language -- we have to prove progress and preservation for both.
Our semantics is essentially small step, but with an implicit context: we keep focusing until we hit a redex. Our formalized semantics is distinguished from many other formalizations in Twelf by the following features. First, the rules of our reduction relations are free from overlapping (which makes the semantics deterministic). Second, the small-step semantics (albeit more involved than the big-step semantics shown for mini-ML and other examples in the Twelf distribution) gives meaningful progress theorems. Many Twelf formalizations do not distinguish well-typed divergent terms from ill-typed ones: both lead to non-terminating reductions. In contrast, in our dynamic semantics non-sensical terms do get stuck rather than diverge; we prove that well-typed terms do not get stuck.
Joint work with Chung-chieh Shan.
E. Moggi and S. Fagorzi. A Monadic Multi-stage Metalanguage. FoSSaCS 2003
Hao Chen and Jonathan S. Shapiro. Using Build-Integrated Static Checking to Preserve Correctness Invariants. CCS'04: Proc. 11th ACM conf. on Computer and Communications Security, pp 288-297, 2004.
The paper describes the application of the finite-state model checker MOPS to assure safety properties in the operating system kernel EROS. One of such properties is the `yield' property: the kernel must not call yield() when interrupts are disabled. EROS permits disabling interrupts by multiple levels, that is, multiple times in succession; each disabling must be balanced by exactly one enabling. This corresponds to so-called recursive locks. One may acquire the same lock multiple times, but then one must release it that many times: lock acquisitions and releases must be properly nested. Safe control flows with recursive locks cannot be modeled by a finite-state machine. In order to use MOPS, the authors had to introduce an approximation and limit the recursion depth, to 5.
Lightweight static capabilities
Explanation of the trusted kernel approach to static safety and of the method to prove its soundness.
oleg-at-pobox.com or oleg-at-okmij.org
Your comments, problem reports, questions are very welcome!
Converted from HSXML by HSXML->HTML