Library ArchSemX86.OperationalX86TSO
From ASCommon Require Import Options.
From ASCommon Require Import Common Exec FMon.
From stdpp Require Import base options.
Require Import X86Inst.
This is an implementation of the x86-TSO operational concurrency model,
as defined in https://www.cl.cam.ac.uk/~pes20/weakmemory/x86tso-paper.pdf
The number of hardware threads
The TSO model internal state
Record mstate := {
regs : vec registerMap threads;
mem : memoryMap;
buf : vec (list buffer_entry) threads;
lock : option (fin threads);
memWritten : gset address;
termThreads : vec bool threads;
}.
regs : vec registerMap threads;
mem : memoryMap;
buf : vec (list buffer_entry) threads;
lock : option (fin threads);
memWritten : gset address;
termThreads : vec bool threads;
}.
Definition read_reg (tid : fin threads) (reg : reg) (state : mstate) :
option (reg_type reg) :=
let regMap := (regs state !!! tid) in
dmap_lookup reg regMap.
Definition write_reg (tid : fin threads) (reg : reg) (val : reg_type reg)
(state : mstate) : mstate :=
set (lookup_total tid ∘ regs) (dmap_insert reg val) state.
Definition no_pending (x : address) (tid : fin threads)
(state : mstate) : bool :=
let buffer := buf state !!! tid in
bool_decide (∀ av ∈ buffer, addr av ≠ x).
Definition buffer_empty (tid : fin threads) (m : mstate) : bool :=
if buf m !!! tid is [] then true else false.
Definition all_buffers_empty (state : mstate) : bool :=
bool_decide (∀ t : fin threads, buffer_empty t state).
Fixpoint read_byte_from_write_buffer_inner (rev_buffer : list buffer_entry)
(goal_addr: address) :
Exec.t mstate string (option (bv 8)) :=
match rev_buffer with
| x :: xs ⇒
let index := Z.to_N (bv_unsigned (goal_addr - (addr x))%bv) in
if bool_decide (index < size x)%N then
mret (Some (bv_extract (8 × index) 8 (val x)))
else read_byte_from_write_buffer_inner xs goal_addr
| _ ⇒ mret None
end.
Definition read_byte_from_write_buffer (tid : fin threads) (addr : address) :
Exec.t mstate string (option (bv 8)) :=
buffer ← mget ((.!!! tid) ∘ buf);
read_byte_from_write_buffer_inner (rev buffer) addr.
Fixpoint add_to_mem_written (addr : address) (size : nat) :
Exec.t mstate string unit :=
match size with
| S size ⇒
mset memWritten (.∪{[addr]});;
add_to_mem_written (addr `+Z` 1)%bv size
| _ ⇒ mret ()
end.
Definition add_to_write_buffer (tid : fin threads) (addr : address)
(size : N) (val : bv (8 × size)) (state : mstate) : mstate :=
set ((.!!! tid) ∘ buf) (.++ [{| addr := addr; size := size; val := val |}])
state.
Definition mem_addr_modified (addr : address) (size : N) (state : mstate) : bool :=
bool_decide (∃ a ∈ addr_range addr size, a ∈ memWritten state).
Definition write_mem (addr : address) (size : N) (val : bv (8 × size)) :
Exec.t mstate string unit :=
opt ← mget (mem_lookup addr size ∘ mem);
guard_or "Memory isn't mapped to write" (is_Some opt);;
mset mem (mem_insert addr size val).
Definition read_mem_byte_with_store_forwarding (tid : fin threads) (addr : address) :
Exec.t mstate string (bv 8) :=
opt ← read_byte_from_write_buffer tid addr;
if opt is Some read then
mret read
else
opt ← mget (mem_lookup_byte addr ∘ mem);
read ← othrow ("Memory not found at " ++ pretty addr)%string opt;
mret read.
Definition read_mem_with_store_forwarding (tid : fin threads) (addr : address)
(size : N) : Exec.t mstate string (bv (8 × size)) :=
read ← mapM
(fun addr ⇒ read_mem_byte_with_store_forwarding tid addr)
(addr_range addr size);
mret (bv_of_bytes (8 × size) read).
Fixpoint write_buffer_to_mem (buffer: list buffer_entry) (tid: fin threads) :
Exec.t mstate string unit :=
match buffer with
| [] ⇒ mret ()
| h :: t ⇒
write_mem (addr h) (size h) (val h);;
write_buffer_to_mem t tid
end.
Definition empty_write_buffer (tid : fin threads) : Exec.t mstate string unit :=
buffer ← mget ((.!!! tid) ∘ buf);
write_buffer_to_mem buffer tid;;
msetv ((.!!! tid) ∘ buf) [].
Definition blocked (tid : fin threads) (m : mstate) : bool :=
if lock m is Some tid' then bool_decide (tid ≠ tid')
else false.
Definition thread_has_lock (tid : fin threads) (m : mstate) : bool :=
if lock m is Some tid' then bool_decide (tid = tid')
else false.
Definition acquire_lock (tid : fin threads) (state : mstate) : mstate :=
setv lock (Some tid) state.
Definition acquire_lock_conditional (tid : fin threads) :
Exec.t mstate string unit :=
lock_status ← mget lock;
guard_discard (lock_status = None);;
'(buffer_is_empty : bool) ← mget (buffer_empty tid);
guard_discard buffer_is_empty;;
mSet (acquire_lock tid).
Definition release_lock (tid : fin threads) (state : mstate) : mstate :=
setv lock None state.
Definition release_lock_conditional (tid : fin threads) :
Exec.t mstate string unit :=
state ← mGet;
guard_discard (thread_has_lock tid state);;
'(buffer_is_empty : bool) ← mget (buffer_empty tid);
guard_discard buffer_is_empty;;
mSet (release_lock tid).
Section RunOutcome.
Context (tid : fin threads) (eager : bool).
Equations run_outcome (call : outcome) : Exec.t mstate string (eff_ret call) :=
| RegRead reg racc ⇒
opt ← mget (read_reg tid reg);
othrow ("Register " ++ pretty reg ++ " not found")%string opt
| RegWrite reg racc val ⇒
opt ← mget (read_reg tid reg);
guard_or ("Writing register " ++ pretty reg ++ " not in initial state")%string (is_Some opt);;
mSet (write_reg tid reg val)
| MemRead (MemReq.make macc addr () size 0) ⇒
if is_ifetch macc then
modified ← mget (mem_addr_modified addr size);
guard_or "IFetch reading from modified memory" (negb modified);;
opt ← mget (mem_lookup addr size ∘ mem);
read ← othrow ("Memory not found at " ++ pretty addr)%string opt;
mret (Ok (read, 0%bv))
else if is_explicit macc then
guard_discard (negb eager);;
is_blocked ← mget (blocked tid);
guard_discard (negb is_blocked);;
(if is_atomic_rmw macc then acquire_lock_conditional tid else mret ());;
read ← read_mem_with_store_forwarding tid addr size;
mret (Ok (read, bv_0 _))
else
mthrow "Memory access type not supported"
| MemRead _ ⇒ mthrow "Unsupported MemRead"
| MemWrite (MemReq.make macc addr () size 0) val _ ⇒
add_to_mem_written addr (N.to_nat size);;
mSet (add_to_write_buffer tid addr size val);;
(if is_atomic_rmw macc then
if eager then
mdiscard
else
empty_write_buffer tid;;
release_lock_conditional tid
else mret ());;
mret (Ok ())
| MemWrite _ _ _ ⇒ mthrow "Unsupported MemWrite"
| Barrier Barrier_MFENCE ⇒
guard_discard (negb eager);;
'(buffer_is_empty : bool) ← mget (buffer_empty tid);
guard_discard buffer_is_empty;;
mret ()
| Barrier _ ⇒ mret ()
| GenericFail msg ⇒ mthrow msg
| _ ⇒ mthrow "Unsupported outcome".
End RunOutcome.
Definition flush_one_item_buffer (tid : fin threads) :
Exec.t mstate string unit :=
buffer ← mget ((.!!! tid) ∘ buf);
match buffer with
| [] ⇒ mdiscard
| h :: t ⇒
write_mem (addr h) (size h) (val h);;
msetv ((.!!! tid) ∘ buf) t
end.
Context (isem : iMon ()).
Section steps.
Context (term : terminationCondition threads).
Exec.t mstate string unit :=
buffer ← mget ((.!!! tid) ∘ buf);
match buffer with
| [] ⇒ mdiscard
| h :: t ⇒
write_mem (addr h) (size h) (val h);;
msetv ((.!!! tid) ∘ buf) t
end.
Context (isem : iMon ()).
Section steps.
Context (term : terminationCondition threads).
Definition execution_step (tid : fin threads) (eager : bool)
: Exec.t mstate string () :=
terminated ← mget ((.!!! tid) ∘ termThreads);
guard_discard (negb terminated);;
cinterp (run_outcome tid eager) isem;;
'regs ← mget ((.!!! tid) ∘ regs);
if regs_terminated (term !!! tid) regs then
msetv ((.!!! tid) ∘ termThreads) true
else
mret ().
: Exec.t mstate string () :=
terminated ← mget ((.!!! tid) ∘ termThreads);
guard_discard (negb terminated);;
cinterp (run_outcome tid eager) isem;;
'regs ← mget ((.!!! tid) ∘ regs);
if regs_terminated (term !!! tid) regs then
msetv ((.!!! tid) ∘ termThreads) true
else
mret ().
Top level transitions
Definition step : Exec.t mstate string (option (fin threads)) :=
tid ← mchoosef (fin threads);
flush_transition ← mchoosef bool;
if (flush_transition : bool) then
lock_status ← mget lock;
guard_discard (lock_status = None);;
flush_one_item_buffer tid;;
mret None
else
execution_step tid false;;
mret (Some tid).
tid ← mchoosef (fin threads);
flush_transition ← mchoosef bool;
if (flush_transition : bool) then
lock_status ← mget lock;
guard_discard (lock_status = None);;
flush_one_item_buffer tid;;
mret None
else
execution_step tid false;;
mret (Some tid).
Definition run_eager_thread_step (tid : fin threads) :
Exec.t mstate string bool :=
'(terminated : bool) ← mget ((.!!! tid) ∘ termThreads);
if terminated then
mret false
else
st ← mGet;
let new_outcome := execution_step tid true st in
if Exec.to_result_list new_outcome is [] then
mret false
else
Exec.lift_res_st new_outcome;;
mret true.
Exec.t mstate string bool :=
'(terminated : bool) ← mget ((.!!! tid) ∘ termThreads);
if terminated then
mret false
else
st ← mGet;
let new_outcome := execution_step tid true st in
if Exec.to_result_list new_outcome is [] then
mret false
else
Exec.lift_res_st new_outcome;;
mret true.
Runs all possible eager transition in a given thread tid.
Returns the remaining fuel
Fixpoint run_eager_thread (fuel : nat) (tid : fin threads) :
Exec.t mstate string nat :=
if fuel is S fuel then
'(instr_ran : bool) ← run_eager_thread_step tid;
if instr_ran then
run_eager_thread fuel tid
else mret (S fuel)
else mthrow "Out of fuel".
Exec.t mstate string nat :=
if fuel is S fuel then
'(instr_ran : bool) ← run_eager_thread_step tid;
if instr_ran then
run_eager_thread fuel tid
else mret (S fuel)
else mthrow "Out of fuel".
Runs all possible transition in all threads.
Definition run_eager_all (fuel : nat) : Exec.t mstate string nat :=
foldlM run_eager_thread fuel (enum (fin threads)).
foldlM run_eager_thread fuel (enum (fin threads)).
Run a non-eager step and then as many eager steps as possible,
assuming no eager step could be taken before the normal step
Definition run_normal_then_eager (fuel : nat) : Exec.t mstate string () :=
eager_thread ← step;
if eager_thread is Some tid then
run_eager_thread fuel tid;;
mret ()
else mret ().
eager_thread ← step;
if eager_thread is Some tid then
run_eager_thread fuel tid;;
mret ()
else mret ().
Definition from_archState (astate : archState threads) : mstate :=
{|
regs := astate.(archState.regs);
mem := astate.(archState.memory);
buf := Vector.const [] threads;
lock := None;
memWritten := ∅;
termThreads :=
vimap (λ tid, regs_terminated (term !!! tid)) astate.(archState.regs);
|}.
Definition to_archState (mstate : mstate) : option (archState threads) :=
if all_buffers_empty mstate && bool_decide (lock mstate = None) then
Some {|
archState.regs := regs mstate;
archState.memory := mem mstate;
archState.address_space := ()
|}
else None.
Definition to_terminated_archState (mstate : mstate) :
option {s : archState threads & archState.is_terminated term s} :=
guard (∀ tid, mstate.(termThreads) !!! tid : bool);;
astate ← (to_archState mstate);
if decide (archState.is_terminated term astate) is left p then
Some (existT astate p)
else None.
End steps.
The unoptimised X86-TSO model. Take one step per instruction or flushing
transitions. Need fuel for all instruction + all flushed writes + 1 for the
terminating step
Definition x86_tso_opmodel : opModel threads :=
let init term initSt := mret (from_archState term initSt) in
let opstep term _ _ :=
fstate ← mget (to_terminated_archState term);
if fstate is Some fs then mret (Some fs) else
step term;;
mret None
in
opModel.Make threads mstate init opstep.
let init term initSt := mret (from_archState term initSt) in
let opstep term _ _ :=
fstate ← mget (to_terminated_archState term);
if fstate is Some fs then mret (Some fs) else
step term;;
mret None
in
opModel.Make threads mstate init opstep.
The X86-TSO model with eager steps. The fuel of of the previous model plus
one is guaranteed to be sufficient but some lower fuel might work
depending on the interleaving of eager and non-eager steps.
Definition x86_tso_opmodel_eager : opModel threads :=
let init term initSt := mret (from_archState term initSt, true) in
let step term _ fuel :=
fstate ← mget (to_terminated_archState term ∘ fst);
if fstate is Some fs then mret (Some fs)
else
initial ← mget snd;
if (initial : bool) then
Exec.liftSt fst $ run_eager_all term fuel;;
msetv snd false;;
mret None
else
Exec.liftSt fst $ run_normal_then_eager term fuel;;
mret None
in
opModel.Make threads (mstate × bool) init step.
End Model.
Arguments mstate : clear implicits.
Arguments x86_tso_opmodel : clear implicits.
Arguments x86_tso_opmodel_eager : clear implicits.
let init term initSt := mret (from_archState term initSt, true) in
let step term _ fuel :=
fstate ← mget (to_terminated_archState term ∘ fst);
if fstate is Some fs then mret (Some fs)
else
initial ← mget snd;
if (initial : bool) then
Exec.liftSt fst $ run_eager_all term fuel;;
msetv snd false;;
mret None
else
Exec.liftSt fst $ run_normal_then_eager term fuel;;
mret None
in
opModel.Make threads (mstate × bool) init step.
End Model.
Arguments mstate : clear implicits.
Arguments x86_tso_opmodel : clear implicits.
Arguments x86_tso_opmodel_eager : clear implicits.
Top-level one-threaded model function that takes fuel (guaranteed
termination) and an instruction monad, and returns a computational set of
all possible final states.
Definition x86_tso_modelc (fuel : nat) (isem : iMon ()) (allow_eager : bool)
: (archModel.c ∅) :=
if allow_eager then
opModel.to_archModel (λ threads, x86_tso_opmodel_eager threads isem) fuel
else
opModel.to_archModel (λ threads, x86_tso_opmodel threads isem) fuel.
: (archModel.c ∅) :=
if allow_eager then
opModel.to_archModel (λ threads, x86_tso_opmodel_eager threads isem) fuel
else
opModel.to_archModel (λ threads, x86_tso_opmodel threads isem) fuel.