adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

aspec+haskell: add accessor names for scheduler_action datatype 

This adds sch_act_target/schActTarget accessor names for the
switch_thread/SwitchToThread constructor of the scheduler_action
datatype at the aspec and Haskell level, respectively

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This commit is contained in:
Michael McInerney 2023-03-22 10:23:23 +10:30 committed by Gerwin Klein
parent c4d673b96d
commit fc44f65175
2 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
spec/abstract/Deterministic_A.thy
View File

@ -107,7 +107,7 @@ text \<open>The current scheduler action,
which is part of the scheduling state.\<close>
datatype scheduler_action =
resume_cur_thread
| switch_thread obj_ref
| switch_thread (sch_act_target : obj_ref)
| choose_new_thread
type_synonym domain = word8

3
spec/haskell/src/SEL4/Object/Structures.lhs
View File

@ -403,7 +403,8 @@ This type is used to represent the required action, if any, of the scheduler nex
\item IPC operations may request that the scheduler switch to a specific thread.
> | SwitchToThread (PPtr TCB)
> | SwitchToThread {
> schActTarget :: PPtr TCB }
> deriving (Eq, Show)