adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
lh-l4v/proof/refine
History
Michael McInerney 4463e9750e SELFOUR-1198: update proofs for correct restart PC 
Fixes a case where a thread can go from Running->Inactive->Restart and
use a restart PC that is out of date. An out of date restart PC occurs
when a thread was transitioned to running after being in a blocked
state, but was never scheduled and so did not execute the traps code
that updates the restart PC.

This also renames relevant register names for consistency across
architectures (FaultIP and NextIP).
 		2019-06-13 11:43:50 +10:00
..
ARM SELFOUR-1198: update proofs for correct restart PC 2019-06-13 11:43:50 +10:00
ARM_HYP SELFOUR-1198: update proofs for correct restart PC 2019-06-13 11:43:50 +10:00
X64 SELFOUR-1198: update proofs for correct restart PC 2019-06-13 11:43:50 +10:00
README.md fix broken README links 2018-01-29 13:24:35 +11:00

README.md

Design Spec Refinement Proof

This proof establishes that seL4's design specification is a formal refinement (i.e. a correct implementation) of its abstract specification. This proof also interweaves the definition and proofs of the global invariant for the design specification, and builds on the Abstract Spec Invariant Proof. It is described in the TPHOLS '08 paper.

Building

Make sure that the L4V_ARCH environment variable is set to the desired target architecture. If in doubt, use L4V_ARCH=ARM.

To build from the l4v/ directory, run:

./isabelle/bin/isabelle build -d . -v -b Refine

Important Theories

The top-level theory where the refinement statement is established over the entire kernel is Refine; the state-relation that relates the state-spaces of the two specifications is defined in StateRelation and the basic correspondence property proved over each kernel function is defined in Corres.