Skip to content

Commit

Permalink
Update LKMM based on "Restrict to-r to read-read address dependency" …
Browse files Browse the repository at this point in the history
…and "Make ppo a subrelation of po" patches (#508)

Signed-off-by: Hernan Ponce de Leon <[email protected]>
  • Loading branch information
hernanponcedeleon authored Sep 6, 2023
1 parent f93d230 commit 5434825
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions cat/linux-kernel.cat
Original file line number Diff line number Diff line change
Expand Up @@ -97,8 +97,8 @@ let dep = addr | data
let rwdep = (dep | ctrl) ; [W]
let overwrite = co | fr
let to-w = rwdep | (overwrite & int) | (addr ; [Plain] ; wmb)
let to-r = addr | (dep ; [Marked] ; rfi)
let ppo = to-r | to-w | fence | (po-unlock-lock-po & int)
let to-r = (addr ; [R]) | (dep ; [Marked] ; rfi)
let ppo = to-r | to-w | (fence & int) | (po-unlock-lock-po & int)

(* Propagation: Ordering from release operations and strong fences. *)
let rmw-sequence = (rf ; rmw)*
Expand Down

0 comments on commit 5434825

Please sign in to comment.