Commits on May 23, 2024

1. spec+proof: use linked lists in the design spec …

   This models the ready queues in the design spec as linked lists
   via the tcbSchedNext and tcbSchedPrev pointers of a TCB, as in the C.
   
   Library functions to update these linked lists are introduced, and used
   to perform all functions which modify the ready queues.
   
   Refinement between the linked lists and the Isabelle lists in the
   abstract spec is handled via the predicate `heap_ls`.
   
   `invs'` has been significantly modified, with the introduction of
   `valid_sched_pointers` and `sym_heap_sched_pointers`. The various
   invariants related to the bitmaps have been collected in the invariant
   `valid_bitmaps`.
   
   This includes a major revision to Orphanage, which now uses the
   tcbQueued field of a TCB to indicate a thread's membership in a
   ready queue, rather than the previous formulation which used
   membership in the set of the Isabelle list.
   
   Co-authored-by: Rafal Kolanski <[email protected]>
   Co-authored-by: Gerwin Klein <[email protected]>
   Signed-off-by: Michael McInerney <[email protected]>

   

   3 people committed May 23, 2024
   Configuration menu

   • View commit details
   • Copy full SHA for d2b566a
   • Browse repository at this point

   Copy the full SHA

   d2b566a View commit details

   Browse the repository at this point in the history