#
c4dc578b |
|
17-Sep-2018 |
Edward Pierzchalski <ed.pierzchalski@data61.csiro.au> |
Fix up proofs after word lemma moves
|
#
d7574020 |
|
20-Sep-2018 |
Edward Pierzchalski <ed.pierzchalski@data61.csiro.au> |
Remove pure word lemmas from proof/* Removes redundant lemmas after moving them up to Word_Lib.
|
#
6b9d9d24 |
|
09-Jun-2018 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
Isabelle2018: new "op x" syntax; now is "(x)" (result of "isabelle update_op -m <dir>")
|
#
bea2e09c |
|
12-Mar-2018 |
Japheth Lim <Japheth.Lim@data61.csiro.au> |
crefine: further update for C-parser change to avoid complex call lvals (JIRA VER-881)
|
#
3a22487c |
|
24-Nov-2017 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
arm: revise scheduler / fastpath / scheduler bitmaps (SELFOUR-242) Colloquially known as "invert-fastpath". Update verification efforts on ARM for the following seL4 changes: - scheduling decisions done in possibleSwitchTo are moved to the scheduler - possibleSwitchTo only checks whether the candidate is valid for a fast switch, not its priority, accepting possible candidates immmediately as a switch-to scheduler action - the scheduler checks the candidate against the current thread and against the bitmaps before making a decision - attemptSwitchTo and switchIfRequiredTo are gone - scheduler is now more complicated, and numerous proofs related to it are rewritten from scratch - fast path now checks ready queues via the scheduler bitmaps - L2 scheduler bitmap order reversed for better cache locality Many iterations between the kernel and verification teams were needed to get this right.
|
#
48b3a8b4 |
|
04-Oct-2017 |
Matthew Brecknell <Matthew.Brecknell@data61.csiro.au> |
update object and field widths for x64, and remove some magic numbers In X64 update the following to match the C kernel: - TCB size-bits (11). - Endpoint size-bits (4). - Guard bits (58). - Message registers. For all architectures, replace magic numbers with defined constants in specifications, and as far as possible in proofs: - tcb_bits in abstract spec. - tcbBlockSizeBits, cteSizeBits, ntfnSizeBits, epSizeBits in Haskell spec, Haskell and C refinement proofs.
|
#
564359b1 |
|
14-Sep-2017 |
Gerwin Klein <gerwin.klein@data61.csiro.au> |
arm crefine: proof updates for bitfield generator changes The name mangling of "v" changes in a few places, and mask_def is occasionally needed where it wasn't before.
|
#
796887d9 |
|
11-Jul-2017 |
Alejandro Gomez-Londono <alejandro.gomez@nicta.com.au> |
Removes all trailing whitespaces
|
#
392d055e |
|
15-May-2017 |
Joel Beeren <joel.beeren@nicta.com.au> |
SELFOUR-748: rename tlb invalidation functions
|
#
284cb43f |
|
04-Jun-2017 |
Alejandro Gomez-Londono <alejandro.gomez@data61.csiro.au> |
arm crefine: Updates clearMemory_setObject_PTE_ccorres to use pteBits
|
#
17776ce6 |
|
04-Jun-2017 |
Alejandro Gomez-Londono <alejandro.gomez@data61.csiro.au> |
arm crefine: Refactors proofs for new definitions (pteBits, pdeBits, etc)
|
#
f00bd94a |
|
30-Mar-2017 |
Rafal Kolanski <rafal.kolanski@nicta.com.au> |
crefine: move crefine/* into crefine/ARM/*
|