adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
1,362 Commits 7 Branches 0 Tags 86 MiB
Commit Graph

22 Commits

Author SHA1 Message Date
Matthew Brecknell a3714e8190 SELFOUR-276: Finish proofs for maximum controlled priority (MCP) 
To finish the proof of refinement to C, the specification for checkPrio
needed strengthening: the checkPrio spec now takes a machine word
argument. In the spec, priorities are still stored as 8-bit quantities,
however. Once the spec was strenthened, it was possible to remove some
redundant checks and mask operations from the C code.

A thread's maximum controlled priority (MCP) determines the maximum
thread priority or MCP it can assign to another thread (or itself).
 2016-10-05 02:43:41 +11:00
Joel Beeren b352769016 SELFOUR-276: Prove refinement to Haskell for MCP 
Also includes fixes to specs and invariants, and initial progress
towards C refinement.

A thread's maximum controlled priority (MCP) determines the maximum
thread priority or MCP it can assign to another thread (or itself).
 2016-10-05 02:43:41 +11:00
Xin,Gao 8d4a8eb238 SELFOUR-421: fix coding style 2016-09-22 19:23:28 +10:00
Xin,Gao 113315d9a6 SELFOUR-421: merge and fix up to ArmConfidentiality proof 2016-09-22 19:21:56 +10:00
Xin,Gao 328846ee1a SELFOUR-421: crefine builds 2016-09-22 19:11:37 +10:00
Xin,Gao 7784e80940 SELFOUR-421: fix refine 2016-09-22 19:11:36 +10:00
Xin,Gao c3be923ca0 SELFOUR-421: a defend version before wild changes 2016-09-22 19:11:36 +10:00
Joel Beeren df877769fc SELFOUR-421: refine done 2016-09-22 19:11:36 +10:00
Joel Beeren 3c223b42fe SELFOUR-421: AInvs done, no added invariants yet 2016-09-22 19:11:29 +10:00
Daniel Matichuk 94f7004f07 arch_split: Refine checking up to end of Finalise_R 2016-04-28 17:16:49 +10:00
Daniel Matichuk 1d20b393c0 arch_split: replaced sublocale with global_naming 2016-04-27 14:32:38 +10:00
Miki Tanaka 6f6c58168c SELFOUR-56: Remove diminish rights from IPC 2016-02-24 13:24:10 +11:00
Matthew Brecknell c65e290a8b Isabelle2016: merge master into 2016 2016-02-16 12:52:24 +11:00
Miki Tanaka b7376a56e2 Isabelle 2016 update: minor fixes 2016-01-15 16:03:30 +11:00
Daniel Matichuk ca808130e6 repair ARM proofs up to Refine after factoring out architecture 2016-01-13 12:02:12 +11:00
Joel Beeren 457a55a831 add arch_tcb object to C, rename aep -> ntfn 2015-11-20 16:02:13 +11:00
Ramana Kumar 0fb88ea01c Merge branch 'master' into aep-merge 
This commit should at least remove merge conflict markers, and the idea
is that at least refine, crefine, drefine, and infoflow (with sorrys)
build. Subsequent commits may be required to fix build issues that I
have not picked up.
 2015-09-10 17:06:45 +10:00
Ramana Kumar d88a931ec7 history squashed patch for aep-binding 2015-09-02 15:43:39 +10:00
Gerwin Klein 7e7d39c24e enable XN in abstract spec; update AInvs and Refine 2014-11-28 08:58:57 +11:00
Thomas Sewell 9b01fada15 Refine working. 2014-08-11 18:51:04 +10:00
Gerwin Klein 1af1d2b67b some of the global Isabelle2014 renames 
option_case -> case_option
sum_case -> case_sum
prod_case -> case_prod
Option.set -> set_option
Option.map -> map_option
option_rel -> rel_option
list_all2_def -> list_all2_iff
map.simps -> list.map
tl.simps -> list.sel(2-3)
the.simps -> option.sel
 2014-08-09 15:39:20 +10:00
Gerwin Klein 2a03e81df4 Import release snapshot. 2014-07-14 21:32:44 +02:00