Skip to content

Commit

Permalink
Minor syntactic change to make the code more readable (semantics is t…
Browse files Browse the repository at this point in the history
…he same)
  • Loading branch information
fshaked committed May 25, 2021
1 parent 055de87 commit 8e34e54
Showing 1 changed file with 9 additions and 9 deletions.
18 changes: 9 additions & 9 deletions src_concurrency_model/machineDefThreadSubsystem.lem
Original file line number Diff line number Diff line change
Expand Up @@ -3258,16 +3258,16 @@ let excl_res_success_action
(state: thread_state 'i)
(iic: instruction_in_context 'i)
(isa_cont: bool -> outcome unit)
()
=
let i = iic.iic_instance in
let i' = <| i with micro_op_state = MOS_plain (isa_cont true) |> in
let i' = if record_success
then <| i' with successful_atomic_store = Just true |>
else i' in
let it' = apply_tree_context iic.context (i', iic.subtree) in
let state' = <| state with instruction_tree = it' |> in
make_thread_cont_res {} {} state'
fun () ->
let i = iic.iic_instance in
let i' = <| i with micro_op_state = MOS_plain (isa_cont true) |> in
let i' = if record_success
then <| i' with successful_atomic_store = Just true |>
else i' in
let it' = apply_tree_context iic.context (i', iic.subtree) in
let state' = <| state with instruction_tree = it' |> in
make_thread_cont_res {} {} state'


let enumerate_excl_res_success_outcome_transition_pop
Expand Down

0 comments on commit 8e34e54

Please sign in to comment.