diff --git a/cat/aarch64fences.cat b/cat/aarch64fences.cat deleted file mode 100644 index 626ee63ce8..0000000000 --- a/cat/aarch64fences.cat +++ /dev/null @@ -1,24 +0,0 @@ -AArch64Fences - -(* Fences *) -let dmb.ish = try fencerel(DMB.ISH) with 0 -let dmb.ishld = try fencerel(DMB.ISHLD) with 0 -let dmb.ishst = try fencerel(DMB.ISHST) with 0 -let dmb.fullsy = try fencerel(DMB.SY) with 0 -let dmb.fullst = try fencerel(DMB.ST) with 0 -let dmb.fullld = try fencerel(DMB.LD) with 0 -let dmb.sy = dmb.fullsy | dmb.ish -let dmb.st = dmb.fullst | dmb.ishst -let dmb.ld = dmb.fullld | dmb.ishld -let dsb.sy = try fencerel(DSB.SY) with 0 -let dsb.st = try fencerel(DSB.ST) with 0 -let dsb.ld = try fencerel(DSB.LD) with 0 -let isb = try fencerel(ISB) with 0 -show dmb.sy,dmb.st,dmb.ld,dsb.sy,sb.st,dsb.ld,dmb,dsb - -(* Dependencies *) -show data,addr -let ctrlisb = try ctrlcfence(ISB) with 0 -show ctrlisb -show isb \ ctrlisb as isb -show ctrl \ ctrlisb as ctrl \ No newline at end of file diff --git a/cat/basic.cat b/cat/basic.cat new file mode 100644 index 0000000000..39d60a1358 --- /dev/null +++ b/cat/basic.cat @@ -0,0 +1,12 @@ +let fr = rf^-1;co | ([R] \ [range(rf)]);loc;[W] + +let po-loc = po & loc + +let rfe = rf & ext +let coe = co & ext +let fre = fr & ext +let rfi = rf & int +let coi = co & int +let fri = fr & int + +let fencerel(F) = po;[F];po diff --git a/cat/c11-orig.cat b/cat/c11-orig.cat index e216b2a4f0..0c99bce685 100644 --- a/cat/c11-orig.cat +++ b/cat/c11-orig.cat @@ -9,6 +9,7 @@ Rewritten by Luc Maranget for herd7 *) +include "basic.cat" include "c11_cos.cat" include "c11_los.cat" diff --git a/cat/c11.cat b/cat/c11.cat index ddd736defd..31c032c097 100644 --- a/cat/c11.cat +++ b/cat/c11.cat @@ -14,6 +14,7 @@ Rewritten by Luc Maranget for herd7 may be missing. As a consequence, reads may have no rf-edge if they read from initial memory. *) +include "basic.cat" include "c11_cos.cat" include "c11_los.cat" diff --git a/cat/cos.cat b/cat/cos.cat new file mode 100644 index 0000000000..d73247c001 --- /dev/null +++ b/cat/cos.cat @@ -0,0 +1,5 @@ +// Herd7 uses cos.cat for generating coherence. +// It usually also defines some derived relations used in many memory models. +// Dartagnan does not need the former; the later is handled by basic.cat below. + +include "basic.cat" \ No newline at end of file diff --git a/cat/imm.cat b/cat/imm.cat index 76a1a7d478..ac3120310c 100644 --- a/cat/imm.cat +++ b/cat/imm.cat @@ -8,6 +8,8 @@ * following GenMC's implementation *) +include "basic.cat" + (* coherence *) let rs = [W];po-loc;[W] | [W];(po-loc?;rf;rmw)* (* release sequence *) (* GenMC uses the same sw definition as RC11 *) diff --git a/cat/linux-kernel.cat b/cat/linux-kernel.cat index ee4da8b4eb..083ee3fac6 100644 --- a/cat/linux-kernel.cat +++ b/cat/linux-kernel.cat @@ -101,8 +101,9 @@ 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 A-cumul(r) = (rfe ; [Marked])? ; r let rmw-sequence = (rf ; rmw)* -let cumul-fence = [Marked] ; ((rfe ; [Marked])? ; (strong-fence | po-rel) | wmb | +let cumul-fence = [Marked] ; (A-cumul(strong-fence | po-rel) | wmb | po-unlock-lock-po) ; [Marked] ; rmw-sequence let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ; [Marked] ; rfe? ; [Marked] diff --git a/cat/lkmm-no-data-race.cat b/cat/lkmm-no-data-race.cat deleted file mode 100644 index 8a2de2320d..0000000000 --- a/cat/lkmm-no-data-race.cat +++ /dev/null @@ -1,154 +0,0 @@ -// SPDX-License-Identifier: GPL-2.0+ -(* - * Copyright (C) 2015 Jade Alglave , - * Copyright (C) 2016 Luc Maranget for Inria - * Copyright (C) 2017 Alan Stern , - * Andrea Parri - * - * An earlier version of this file appeared in the companion webpage for - * "Frightening small children and disconcerting grown-ups: Concurrency - * in the Linux kernel" by Alglave, Maranget, McKenney, Parri, and Stern, - * which appeared in ASPLOS 2018. - *) - -"Linux-kernel memory consistency model" - -(* - * File "lock.cat" handles locks and is experimental. - * It can be replaced by include "cos.cat" for tests that do not use locks. - *) - -include "lock.cat" - -(* Compute marked and plain memory accesses *) -let Marked = (~M) | IW | Once | Release | Acquire | (RMW & R) | (RMW & W) | - LKR | LKW | UL | LF | RL | RU -let Plain = M \ Marked - -(*******************) -(* Basic relations *) -(*******************) - -(* Release Acquire *) -let acq-po = [Acquire] ; po ; [M] -let po-rel = [M] ; po ; [Release] -let po-unlock-lock-po = po ; [UL] ; (po|rf) ; [LKR] ; po - -(* Fences *) -let R4rmb = R \ Noreturn (* Reads for which rmb works *) -let rmb = [R4rmb] ; fencerel(Rmb) ; [R4rmb] -let wmb = [W] ; fencerel(Wmb) ; [W] -let mb = ([M] ; fencerel(Mb) ; [M]) | - ([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) | - ([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) | - ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) | - ([M] ; po ; [UL] ; (co | po) ; [LKW] ; - fencerel(After-unlock-lock) ; [M]) -let gp = po ; [Sync-rcu | Sync-srcu] ; po? -let strong-fence = mb | gp - -let nonrw-fence = strong-fence | po-rel | acq-po -let fence = nonrw-fence | wmb | rmb - -(**********************************) -(* Fundamental coherence ordering *) -(**********************************) - -(* Sequential Consistency Per Variable *) -let com = rf | co | fr -acyclic po-loc | com as coherence - -(* Atomic Read-Modify-Write *) -empty rmw & (fre ; coe) as atomic - -(**********************************) -(* Instruction execution ordering *) -(**********************************) - -(* Preserved Program Order *) -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) - -(* Propagation: Ordering from release operations and strong fences. *) -let cumul-fence = [Marked] ; ((rfe ; [Marked])? ; (strong-fence | po-rel) | wmb | po-unlock-lock-po) ; [Marked] -let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ; [Marked] ; rfe? ; [Marked] - -(* - * Happens Before: Ordering from the passage of time. - * No fences needed here for prop because relation confined to one process. - *) -let hb = [Marked] ; (ppo | rfe | ((prop \ id) & int)) ; [Marked] -acyclic hb as happens-before - -(****************************************) -(* Write and fence propagation ordering *) -(****************************************) - -(* Propagation: Each non-rf link needs a strong fence. *) -let pb = prop ; strong-fence ; hb* ; [Marked] -acyclic pb as propagation - -(*******) -(* RCU *) -(*******) - -(* - * Effects of read-side critical sections proceed from the rcu_read_unlock() - * or srcu_read_unlock() backwards on the one hand, and from the - * rcu_read_lock() or srcu_read_lock() forwards on the other hand. - * - * In the definition of rcu-fence below, the po term at the left-hand side - * of each disjunct and the po? term at the right-hand end have been factored - * out. They have been moved into the definitions of rcu-link and rb. - * This was necessary in order to apply the "& loc" tests correctly. - *) -let rcu-gp = [Sync-rcu] (* Compare with gp *) -let srcu-gp = [Sync-srcu] -let rcu-rscsi = rcu-rscs^-1 -// NOTE: We don't support SRCU -let srcu-rscsi = 0 - -(* - * The synchronize_rcu() strong fence is special in that it can order not - * one but two non-rf relations, but only in conjunction with an RCU - * read-side critical section. - *) -let rcu-link = po? ; hb* ; pb* ; prop ; po - -(* - * Any sequence containing at least as many grace periods as RCU read-side - * critical sections (joined by rcu-link) induces order like a generalized - * inter-CPU strong fence. - * Likewise for SRCU grace periods and read-side critical sections, provided - * the synchronize_srcu() and srcu_read_[un]lock() calls refer to the same - * struct srcu_struct location. - *) -let rec rcu-order = rcu-gp | srcu-gp | - (rcu-gp ; rcu-link ; rcu-rscsi) | - ((srcu-gp ; rcu-link ; srcu-rscsi) & loc) | - (rcu-rscsi ; rcu-link ; rcu-gp) | - ((srcu-rscsi ; rcu-link ; srcu-gp) & loc) | - (rcu-gp ; rcu-link ; rcu-order ; rcu-link ; rcu-rscsi) | - ((srcu-gp ; rcu-link ; rcu-order ; rcu-link ; srcu-rscsi) & loc) | - (rcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; rcu-gp) | - ((srcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; srcu-gp) & loc) | - (rcu-order ; rcu-link ; rcu-order) -let rcu-fence = po ; rcu-order ; po? - -(* rb orders instructions just as pb does *) -let rb = prop ; rcu-fence ; hb* ; pb* ; [Marked] - -irreflexive rb as rcu - -(* - * The happens-before, propagation, and rcu constraints are all - * expressions of temporal ordering. They could be replaced by - * a single constraint on an "executes-before" relation, xb: - * - * let xb = hb | pb | rb - * acyclic xb as executes-before - *) diff --git a/cat/lkmm/README.md b/cat/lkmm/README.md deleted file mode 100644 index 83bd0fe816..0000000000 --- a/cat/lkmm/README.md +++ /dev/null @@ -1,8 +0,0 @@ -This folder contains different variants of the Linux Kernel Memory Model (LKMM). -The models have been slighlty modified (*) to be used with Dartagnan. - -- lkmm-v00: official version up to version 6.2 of the kernel. -- lkmm-v01: updated via [this](https://lkml.org/lkml/2022/11/16/1555) patch. -- lkmm-v02: updated via [this](https://lkml.org/lkml/2022/12/1/465) patch. - -(*) Dartagnan neither supports bell files (thus definitions like `Marked` and `Plain` were moved to the cat file) nor it allows to "update relations on the fly" (thus we use `update-fence` and `update-strong-fence`). \ No newline at end of file diff --git a/cat/lkmm/lkmm-v00.cat b/cat/lkmm/lkmm-v00.cat deleted file mode 100644 index c954b1ba05..0000000000 --- a/cat/lkmm/lkmm-v00.cat +++ /dev/null @@ -1,207 +0,0 @@ -// SPDX-License-Identifier: GPL-2.0+ -(* - * Copyright (C) 2015 Jade Alglave , - * Copyright (C) 2016 Luc Maranget for Inria - * Copyright (C) 2017 Alan Stern , - * Andrea Parri - * - * An earlier version of this file appeared in the companion webpage for - * "Frightening small children and disconcerting grown-ups: Concurrency - * in the Linux kernel" by Alglave, Maranget, McKenney, Parri, and Stern, - * which appeared in ASPLOS 2018. - *) - -"Linux-kernel memory consistency model" - -(* - * File "lock.cat" handles locks and is experimental. - * It can be replaced by include "cos.cat" for tests that do not use locks. - *) - -include "lock.cat" - -(* Compute marked and plain memory accesses *) -let Marked = (~M) | IW | Once | Release | Acquire | (RMW & R) | (RMW & W) | - LKR | LKW | UL | LF | RL | RU -let Plain = M \ Marked - -(*******************) -(* Basic relations *) -(*******************) - -(* Release Acquire *) -let acq-po = [Acquire] ; po ; [M] -let po-rel = [M] ; po ; [Release] -let po-unlock-lock-po = po ; [UL] ; (po|rf) ; [LKR] ; po - -(* Fences *) -let R4rmb = R \ Noreturn (* Reads for which rmb works *) -let rmb = [R4rmb] ; fencerel(Rmb) ; [R4rmb] -let wmb = [W] ; fencerel(Wmb) ; [W] -let mb = ([M] ; fencerel(Mb) ; [M]) | - ([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) | - ([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) | - ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) | - ([M] ; po ; [UL] ; (co | po) ; [LKW] ; - fencerel(After-unlock-lock) ; [M]) -let gp = po ; [Sync-rcu | Sync-srcu] ; po? -let strong-fence = mb | gp - -let nonrw-fence = strong-fence | po-rel | acq-po -let fence = nonrw-fence | wmb | rmb - -(**********************************) -(* Fundamental coherence ordering *) -(**********************************) - -(* Sequential Consistency Per Variable *) -let com = rf | co | fr -acyclic po-loc | com as coherence - -(* Atomic Read-Modify-Write *) -empty rmw & (fre ; coe) as atomic - -(**********************************) -(* Instruction execution ordering *) -(**********************************) - -(* Preserved Program Order *) -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) - -(* Propagation: Ordering from release operations and strong fences. *) -let cumul-fence = [Marked] ; ((rfe ; [Marked])? ; (strong-fence | po-rel) | wmb | po-unlock-lock-po) ; [Marked] -let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ; [Marked] ; rfe? ; [Marked] - -(* - * Happens Before: Ordering from the passage of time. - * No fences needed here for prop because relation confined to one process. - *) -let hb = [Marked] ; (ppo | rfe | ((prop \ id) & int)) ; [Marked] -acyclic hb as happens-before - -(****************************************) -(* Write and fence propagation ordering *) -(****************************************) - -(* Propagation: Each non-rf link needs a strong fence. *) -let pb = prop ; strong-fence ; hb* ; [Marked] -acyclic pb as propagation - -(*******) -(* RCU *) -(*******) - -(* - * Effects of read-side critical sections proceed from the rcu_read_unlock() - * or srcu_read_unlock() backwards on the one hand, and from the - * rcu_read_lock() or srcu_read_lock() forwards on the other hand. - * - * In the definition of rcu-fence below, the po term at the left-hand side - * of each disjunct and the po? term at the right-hand end have been factored - * out. They have been moved into the definitions of rcu-link and rb. - * This was necessary in order to apply the "& loc" tests correctly. - *) -let rcu-gp = [Sync-rcu] (* Compare with gp *) -let srcu-gp = [Sync-srcu] -let rcu-rscsi = rcu-rscs^-1 -// NOTE: We don't support SRCU -let srcu-rscsi = 0 - -(* - * The synchronize_rcu() strong fence is special in that it can order not - * one but two non-rf relations, but only in conjunction with an RCU - * read-side critical section. - *) -let rcu-link = po? ; hb* ; pb* ; prop ; po - -(* - * Any sequence containing at least as many grace periods as RCU read-side - * critical sections (joined by rcu-link) induces order like a generalized - * inter-CPU strong fence. - * Likewise for SRCU grace periods and read-side critical sections, provided - * the synchronize_srcu() and srcu_read_[un]lock() calls refer to the same - * struct srcu_struct location. - *) -let rec rcu-order = rcu-gp | srcu-gp | - (rcu-gp ; rcu-link ; rcu-rscsi) | - ((srcu-gp ; rcu-link ; srcu-rscsi) & loc) | - (rcu-rscsi ; rcu-link ; rcu-gp) | - ((srcu-rscsi ; rcu-link ; srcu-gp) & loc) | - (rcu-gp ; rcu-link ; rcu-order ; rcu-link ; rcu-rscsi) | - ((srcu-gp ; rcu-link ; rcu-order ; rcu-link ; srcu-rscsi) & loc) | - (rcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; rcu-gp) | - ((srcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; srcu-gp) & loc) | - (rcu-order ; rcu-link ; rcu-order) -let rcu-fence = po ; rcu-order ; po? -let update-fence = fence | rcu-fence -let update-strong-fence = strong-fence | rcu-fence - -(* rb orders instructions just as pb does *) -let rb = prop ; rcu-fence ; hb* ; pb* ; [Marked] - -irreflexive rb as rcu - -(* - * The happens-before, propagation, and rcu constraints are all - * expressions of temporal ordering. They could be replaced by - * a single constraint on an "executes-before" relation, xb: - * - * let xb = hb | pb | rb - * acyclic xb as executes-before - *) - -(*********************************) -(* Plain accesses and data races *) -(*********************************) - -let barrier = fencerel(Barrier | Rmb | Wmb | Mb | Sync-rcu | Sync-srcu | - Before-atomic | After-atomic | Acquire | Release | - Rcu-lock | Rcu-unlock | Srcu-lock | Srcu-unlock) | - (po ; [Release]) | ([Acquire] ; po) - -(* Warn about plain writes and marked accesses in the same region *) -let mixed-accesses = ([Plain & W] ; (po-loc \ barrier) ; [Marked]) | - ([Marked] ; (po-loc \ barrier) ; [Plain & W]) -flag ~empty mixed-accesses as mixed-accesses - -(* Executes-before and visibility *) -let xbstar = (hb | pb | rb)* -let vis = cumul-fence* ; rfe? ; [Marked] ; - ((update-strong-fence ; [Marked] ; xbstar) | (xbstar & int)) - -(* Boundaries for lifetimes of plain accesses *) -let w-pre-bounded = [Marked] ; (addr |update-fence)? -let r-pre-bounded = [Marked] ; (addr | nonrw-fence | - ([R4rmb] ; fencerel(Rmb) ; [~Noreturn]))? -let w-post-bounded =update-fence? ; [Marked] -let r-post-bounded = (nonrw-fence | ([~Noreturn] ; fencerel(Rmb) ; [R4rmb]))? ; - [Marked] - -(* Visibility and executes-before for plain accesses *) -let ww-vis =update-fence | (update-strong-fence ; xbstar ; w-pre-bounded) | - (w-post-bounded ; vis ; w-pre-bounded) -let wr-vis =update-fence | (update-strong-fence ; xbstar ; r-pre-bounded) | - (w-post-bounded ; vis ; r-pre-bounded) -let rw-xbstar =update-fence | (r-post-bounded ; xbstar ; w-pre-bounded) - -(* Potential races *) -let pre-race = ext & ((Plain * M) | ((M \ IW) * Plain)) - -(* Coherence requirements for plain accesses *) -let wr-incoh = pre-race & rf & rw-xbstar^-1 -let rw-incoh = pre-race & fr & wr-vis^-1 -let ww-incoh = pre-race & co & ww-vis^-1 -empty (wr-incoh | rw-incoh | ww-incoh) as plain-coherence - -//(* Actual races *) -let ww-nonrace = ww-vis & ((Marked * W) | rw-xbstar) & ((W * Marked) | wr-vis) -let ww-race = (pre-race & co) \ ww-nonrace -let wr-race = (pre-race & (co? ; rf)) \ wr-vis \ rw-xbstar^-1 -let rw-race = (pre-race & fr) \ rw-xbstar - -flag ~empty (ww-race | wr-race | rw-race) as data-race diff --git a/cat/lkmm/lkmm-v01.cat b/cat/lkmm/lkmm-v01.cat deleted file mode 100644 index a4d9b983f5..0000000000 --- a/cat/lkmm/lkmm-v01.cat +++ /dev/null @@ -1,209 +0,0 @@ -// SPDX-License-Identifier: GPL-2.0+ -(* - * Copyright (C) 2015 Jade Alglave , - * Copyright (C) 2016 Luc Maranget for Inria - * Copyright (C) 2017 Alan Stern , - * Andrea Parri - * - * An earlier version of this file appeared in the companion webpage for - * "Frightening small children and disconcerting grown-ups: Concurrency - * in the Linux kernel" by Alglave, Maranget, McKenney, Parri, and Stern, - * which appeared in ASPLOS 2018. - *) - -"Linux-kernel memory consistency model" - -(* - * File "lock.cat" handles locks and is experimental. - * It can be replaced by include "cos.cat" for tests that do not use locks. - *) - -include "lock.cat" - -(* Compute marked and plain memory accesses *) -let Marked = (~M) | IW | Once | Release | Acquire | (RMW & R) | (RMW & W) | - LKR | LKW | UL | LF | RL | RU -let Plain = M \ Marked - -(*******************) -(* Basic relations *) -(*******************) - -(* Release Acquire *) -let acq-po = [Acquire] ; po ; [M] -let po-rel = [M] ; po ; [Release] -let po-unlock-lock-po = po ; [UL] ; (po|rf) ; [LKR] ; po - -(* Fences *) -let R4rmb = R \ Noreturn (* Reads for which rmb works *) -let rmb = [R4rmb] ; fencerel(Rmb) ; [R4rmb] -let wmb = [W] ; fencerel(Wmb) ; [W] -let mb = ([M] ; fencerel(Mb) ; [M]) | - ([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) | - ([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) | - ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) | - ([M] ; po ; [UL] ; (co | po) ; [LKW] ; - fencerel(After-unlock-lock) ; [M]) -let gp = po ; [Sync-rcu | Sync-srcu] ; po? -let strong-fence = mb | gp - -let nonrw-fence = strong-fence | po-rel | acq-po -let fence = nonrw-fence | wmb | rmb -let barrier = fencerel(Barrier | Rmb | Wmb | Mb | Sync-rcu | Sync-srcu | - Before-atomic | After-atomic | Acquire | Release | - Rcu-lock | Rcu-unlock | Srcu-lock | Srcu-unlock) | - (po ; [Release]) | ([Acquire] ; po) - -(**********************************) -(* Fundamental coherence ordering *) -(**********************************) - -(* Sequential Consistency Per Variable *) -let com = rf | co | fr -acyclic po-loc | com as coherence - -(* Atomic Read-Modify-Write *) -empty rmw & (fre ; coe) as atomic - -(**********************************) -(* Instruction execution ordering *) -(**********************************) - -(* Preserved Program Order *) -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) - -(* Propagation: Ordering from release operations and strong fences. *) -let rmw-sequence = (rf ; rmw)* -let cumul-fence = [Marked] ; ((rfe ; [Marked])? ; (strong-fence | po-rel) | wmb | - po-unlock-lock-po) ; [Marked] ; rmw-sequence -let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ; - [Marked] ; rfe? ; [Marked] - -(* - * Happens Before: Ordering from the passage of time. - * No fences needed here for prop because relation confined to one process. - *) -let hb = [Marked] ; (ppo | rfe | ((prop \ id) & int)) ; [Marked] -acyclic hb as happens-before - -(****************************************) -(* Write and fence propagation ordering *) -(****************************************) - -(* Propagation: Each non-rf link needs a strong fence. *) -let pb = prop ; strong-fence ; hb* ; [Marked] -acyclic pb as propagation - -(*******) -(* RCU *) -(*******) - -(* - * Effects of read-side critical sections proceed from the rcu_read_unlock() - * or srcu_read_unlock() backwards on the one hand, and from the - * rcu_read_lock() or srcu_read_lock() forwards on the other hand. - * - * In the definition of rcu-fence below, the po term at the left-hand side - * of each disjunct and the po? term at the right-hand end have been factored - * out. They have been moved into the definitions of rcu-link and rb. - * This was necessary in order to apply the "& loc" tests correctly. - *) -let rcu-gp = [Sync-rcu] (* Compare with gp *) -let srcu-gp = [Sync-srcu] -let rcu-rscsi = rcu-rscs^-1 -// NOTE: We don't support SRCU -let srcu-rscsi = 0 - -(* - * The synchronize_rcu() strong fence is special in that it can order not - * one but two non-rf relations, but only in conjunction with an RCU - * read-side critical section. - *) -let rcu-link = po? ; hb* ; pb* ; prop ; po - -(* - * Any sequence containing at least as many grace periods as RCU read-side - * critical sections (joined by rcu-link) induces order like a generalized - * inter-CPU strong fence. - * Likewise for SRCU grace periods and read-side critical sections, provided - * the synchronize_srcu() and srcu_read_[un]lock() calls refer to the same - * struct srcu_struct location. - *) -let rec rcu-order = rcu-gp | srcu-gp | - (rcu-gp ; rcu-link ; rcu-rscsi) | - ((srcu-gp ; rcu-link ; srcu-rscsi) & loc) | - (rcu-rscsi ; rcu-link ; rcu-gp) | - ((srcu-rscsi ; rcu-link ; srcu-gp) & loc) | - (rcu-gp ; rcu-link ; rcu-order ; rcu-link ; rcu-rscsi) | - ((srcu-gp ; rcu-link ; rcu-order ; rcu-link ; srcu-rscsi) & loc) | - (rcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; rcu-gp) | - ((srcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; srcu-gp) & loc) | - (rcu-order ; rcu-link ; rcu-order) -let rcu-fence = po ; rcu-order ; po? -let update-fence = fence | rcu-fence -let update-strong-fence = strong-fence | rcu-fence - -(* rb orders instructions just as pb does *) -let rb = prop ; rcu-fence ; hb* ; pb* ; [Marked] - -irreflexive rb as rcu - -(* - * The happens-before, propagation, and rcu constraints are all - * expressions of temporal ordering. They could be replaced by - * a single constraint on an "executes-before" relation, xb: - * - * let xb = hb | pb | rb - * acyclic xb as executes-before - *) - -(*********************************) -(* Plain accesses and data races *) -(*********************************) - -(* Warn about plain writes and marked accesses in the same region *) -let mixed-accesses = ([Plain & W] ; (po-loc \ barrier) ; [Marked]) | - ([Marked] ; (po-loc \ barrier) ; [Plain & W]) -flag ~empty mixed-accesses as mixed-accesses - -(* Executes-before and visibility *) -let xbstar = (hb | pb | rb)* -let vis = cumul-fence* ; rfe? ; [Marked] ; - ((update-strong-fence ; [Marked] ; xbstar) | (xbstar & int)) - -(* Boundaries for lifetimes of plain accesses *) -let w-pre-bounded = [Marked] ; (addr | update-fence)? -let r-pre-bounded = [Marked] ; (addr | nonrw-fence | - ([R4rmb] ; fencerel(Rmb) ; [~Noreturn]))? -let w-post-bounded = update-fence? ; rmw-sequence -let r-post-bounded = (nonrw-fence | ([~Noreturn] ; fencerel(Rmb) ; [R4rmb]))? ; - [Marked] - -(* Visibility and executes-before for plain accesses *) -let ww-vis = update-fence | (update-strong-fence ; xbstar ; w-pre-bounded) | - (w-post-bounded ; vis ; w-pre-bounded) -let wr-vis = update-fence | (update-strong-fence ; xbstar ; r-pre-bounded) | - (w-post-bounded ; vis ; r-pre-bounded) -let rw-xbstar = update-fence | (r-post-bounded ; xbstar ; w-pre-bounded) - -(* Potential races *) -let pre-race = ext & ((Plain * M) | ((M \ IW) * Plain)) - -(* Coherence requirements for plain accesses *) -let wr-incoh = pre-race & rf & rw-xbstar^-1 -let rw-incoh = pre-race & fr & wr-vis^-1 -let ww-incoh = pre-race & co & ww-vis^-1 -empty (wr-incoh | rw-incoh | ww-incoh) as plain-coherence - -(* Actual races *) -let ww-nonrace = ww-vis & ((Marked * W) | rw-xbstar) & ((W * Marked) | wr-vis) -let ww-race = (pre-race & co) \ ww-nonrace -let wr-race = (pre-race & (co? ; rf)) \ wr-vis \ rw-xbstar^-1 -let rw-race = (pre-race & fr) \ rw-xbstar - -flag ~empty (ww-race | wr-race | rw-race) as data-race \ No newline at end of file diff --git a/cat/lkmm/lkmm-v02.cat b/cat/lkmm/lkmm-v02.cat deleted file mode 100644 index e93320c77c..0000000000 --- a/cat/lkmm/lkmm-v02.cat +++ /dev/null @@ -1,216 +0,0 @@ -// SPDX-License-Identifier: GPL-2.0+ -(* - * Copyright (C) 2015 Jade Alglave , - * Copyright (C) 2016 Luc Maranget for Inria - * Copyright (C) 2017 Alan Stern , - * Andrea Parri - * - * An earlier version of this file appeared in the companion webpage for - * "Frightening small children and disconcerting grown-ups: Concurrency - * in the Linux kernel" by Alglave, Maranget, McKenney, Parri, and Stern, - * which appeared in ASPLOS 2018. - *) - -"Linux-kernel memory consistency model" - -(* - * File "lock.cat" handles locks and is experimental. - * It can be replaced by include "cos.cat" for tests that do not use locks. - *) - -include "lock.cat" - -(* Compute marked and plain memory accesses *) -let Marked = (~M) | IW | Once | Release | Acquire | (RMW & R) | (RMW & W) | - LKR | LKW | UL | LF | RL | RU -let Plain = M \ Marked - -(* Redefine dependencies to include dependencies carried -* through unmarked accesses *) -let carry-dep = (data ; rfi)* -let cd-addr = carry-dep ; addr -let cd-ctrl = carry-dep ; ctrl -let cd-data = carry-dep ; data - -(*******************) -(* Basic relations *) -(*******************) - -(* Release Acquire *) -let acq-po = [Acquire] ; po ; [M] -let po-rel = [M] ; po ; [Release] -let po-unlock-lock-po = po ; [UL] ; (po|rf) ; [LKR] ; po - -(* Fences *) -let R4rmb = R \ Noreturn (* Reads for which rmb works *) -let rmb = [R4rmb] ; fencerel(Rmb) ; [R4rmb] -let wmb = [W] ; fencerel(Wmb) ; [W] -let mb = ([M] ; fencerel(Mb) ; [M]) | - ([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) | - ([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) | - ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) | - ([M] ; po ; [UL] ; (co | po) ; [LKW] ; - fencerel(After-unlock-lock) ; [M]) -let gp = po ; [Sync-rcu | Sync-srcu] ; po? -let strong-fence = mb | gp - -let nonrw-fence = strong-fence | po-rel | acq-po -let fence = nonrw-fence | wmb | rmb -let barrier = fencerel(Barrier | Rmb | Wmb | Mb | Sync-rcu | Sync-srcu | - Before-atomic | After-atomic | Acquire | Release | - Rcu-lock | Rcu-unlock | Srcu-lock | Srcu-unlock) | - (po ; [Release]) | ([Acquire] ; po) - -(**********************************) -(* Fundamental coherence ordering *) -(**********************************) - -(* Sequential Consistency Per Variable *) -let com = rf | co | fr -acyclic po-loc | com as coherence - -(* Atomic Read-Modify-Write *) -empty rmw & (fre ; coe) as atomic - -(**********************************) -(* Instruction execution ordering *) -(**********************************) - -(* Preserved Program Order *) -let dep = cd-addr | cd-data -let rwdep = (dep | cd-ctrl) ; [W] -let overwrite = co | fr -let to-w = rwdep | (overwrite & int) | (cd-addr ; [Plain] ; wmb) -let to-r = cd-addr | (dep ; [Marked] ; rfi) -let ppo = to-r | to-w | fence | (po-unlock-lock-po & int) - -(* Propagation: Ordering from release operations and strong fences. *) -let rmw-sequence = (rf ; rmw)* -let cumul-fence = [Marked] ; ((rfe ; [Marked])? ; (strong-fence | po-rel) | wmb | - po-unlock-lock-po) ; [Marked] ; rmw-sequence -let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ; - [Marked] ; rfe? ; [Marked] - -(* - * Happens Before: Ordering from the passage of time. - * No fences needed here for prop because relation confined to one process. - *) -let hb = [Marked] ; (ppo | rfe | ((prop \ id) & int)) ; [Marked] -acyclic hb as happens-before - -(****************************************) -(* Write and fence propagation ordering *) -(****************************************) - -(* Propagation: Each non-rf link needs a strong fence. *) -let pb = prop ; strong-fence ; hb* ; [Marked] -acyclic pb as propagation - -(*******) -(* RCU *) -(*******) - -(* - * Effects of read-side critical sections proceed from the rcu_read_unlock() - * or srcu_read_unlock() backwards on the one hand, and from the - * rcu_read_lock() or srcu_read_lock() forwards on the other hand. - * - * In the definition of rcu-fence below, the po term at the left-hand side - * of each disjunct and the po? term at the right-hand end have been factored - * out. They have been moved into the definitions of rcu-link and rb. - * This was necessary in order to apply the "& loc" tests correctly. - *) -let rcu-gp = [Sync-rcu] (* Compare with gp *) -let srcu-gp = [Sync-srcu] -let rcu-rscsi = rcu-rscs^-1 -// NOTE: We don't support SRCU -let srcu-rscsi = 0 - -(* - * The synchronize_rcu() strong fence is special in that it can order not - * one but two non-rf relations, but only in conjunction with an RCU - * read-side critical section. - *) -let rcu-link = po? ; hb* ; pb* ; prop ; po - -(* - * Any sequence containing at least as many grace periods as RCU read-side - * critical sections (joined by rcu-link) induces order like a generalized - * inter-CPU strong fence. - * Likewise for SRCU grace periods and read-side critical sections, provided - * the synchronize_srcu() and srcu_read_[un]lock() calls refer to the same - * struct srcu_struct location. - *) -let rec rcu-order = rcu-gp | srcu-gp | - (rcu-gp ; rcu-link ; rcu-rscsi) | - ((srcu-gp ; rcu-link ; srcu-rscsi) & loc) | - (rcu-rscsi ; rcu-link ; rcu-gp) | - ((srcu-rscsi ; rcu-link ; srcu-gp) & loc) | - (rcu-gp ; rcu-link ; rcu-order ; rcu-link ; rcu-rscsi) | - ((srcu-gp ; rcu-link ; rcu-order ; rcu-link ; srcu-rscsi) & loc) | - (rcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; rcu-gp) | - ((srcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; srcu-gp) & loc) | - (rcu-order ; rcu-link ; rcu-order) -let rcu-fence = po ; rcu-order ; po? -let update-fence = fence | rcu-fence -let update-strong-fence = strong-fence | rcu-fence - -(* rb orders instructions just as pb does *) -let rb = prop ; rcu-fence ; hb* ; pb* ; [Marked] - -irreflexive rb as rcu - -(* - * The happens-before, propagation, and rcu constraints are all - * expressions of temporal ordering. They could be replaced by - * a single constraint on an "executes-before" relation, xb: - * - * let xb = hb | pb | rb - * acyclic xb as executes-before - *) - -(*********************************) -(* Plain accesses and data races *) -(*********************************) - -(* Warn about plain writes and marked accesses in the same region *) -let mixed-accesses = ([Plain & W] ; (po-loc \ barrier) ; [Marked]) | - ([Marked] ; (po-loc \ barrier) ; [Plain & W]) -flag ~empty mixed-accesses as mixed-accesses - -(* Executes-before and visibility *) -let xbstar = (hb | pb | rb)* -let vis = cumul-fence* ; rfe? ; [Marked] ; - ((update-strong-fence ; [Marked] ; xbstar) | (xbstar & int)) - -(* Boundaries for lifetimes of plain accesses *) -let w-pre-bounded = [Marked] ; (cd-addr | update-fence)? -let r-pre-bounded = [Marked] ; (cd-addr | nonrw-fence | - ([R4rmb] ; fencerel(Rmb) ; [~Noreturn]))? -let w-post-bounded = update-fence? ; rmw-sequence -let r-post-bounded = (nonrw-fence | ([~Noreturn] ; fencerel(Rmb) ; [R4rmb]))? ; - [Marked] - -(* Visibility and executes-before for plain accesses *) -let ww-vis = update-fence | (update-strong-fence ; xbstar ; w-pre-bounded) | - (w-post-bounded ; vis ; w-pre-bounded) -let wr-vis = update-fence | (update-strong-fence ; xbstar ; r-pre-bounded) | - (w-post-bounded ; vis ; r-pre-bounded) -let rw-xbstar = update-fence | (r-post-bounded ; xbstar ; w-pre-bounded) - -(* Potential races *) -let pre-race = ext & ((Plain * M) | ((M \ IW) * Plain)) - -(* Coherence requirements for plain accesses *) -let wr-incoh = pre-race & rf & rw-xbstar^-1 -let rw-incoh = pre-race & fr & wr-vis^-1 -let ww-incoh = pre-race & co & ww-vis^-1 -empty (wr-incoh | rw-incoh | ww-incoh) as plain-coherence - -(* Actual races *) -let ww-nonrace = ww-vis & ((Marked * W) | rw-xbstar) & ((W * Marked) | wr-vis) -let ww-race = (pre-race & co) \ ww-nonrace -let wr-race = (pre-race & (co? ; rf)) \ wr-vis \ rw-xbstar^-1 -let rw-race = (pre-race & fr) \ rw-xbstar - -flag ~empty (ww-race | wr-race | rw-race) as data-race \ No newline at end of file diff --git a/cat/lock.cat b/cat/lock.cat index 305ded17e7..c8a83e5457 100644 --- a/cat/lock.cat +++ b/cat/lock.cat @@ -1,146 +1,148 @@ -// SPDX-License-Identifier: GPL-2.0+ -(* - * Copyright (C) 2016 Luc Maranget for Inria - * Copyright (C) 2017 Alan Stern - *) - -(* - * Generate coherence orders and handle lock operations - * - * Warning: spin_is_locked() crashes herd7 versions strictly before 7.48. - * spin_is_locked() is functional from herd7 version 7.49. - *) - -include "cross.cat" - -(* - * The lock-related events generated by herd are as follows: - * - * LKR Lock-Read: the read part of a spin_lock() or successful - * spin_trylock() read-modify-write event pair - * LKW Lock-Write: the write part of a spin_lock() or successful - * spin_trylock() RMW event pair - * UL Unlock: a spin_unlock() event - * LF Lock-Fail: a failed spin_trylock() event - * RL Read-Locked: a spin_is_locked() event which returns True - * RU Read-Unlocked: a spin_is_locked() event which returns False - * - * LKR and LKW events always come paired, like all RMW event sequences. - * - * LKR, LF, RL, and RU are read events; LKR has Acquire ordering. - * LKW and UL are write events; UL has Release ordering. - * LKW, LF, RL, and RU have no ordering properties. - *) - -(* Backward compatibility *) -let RL = try RL with emptyset -let RU = try RU with emptyset - -(* Treat RL as a kind of LF: a read with no ordering properties *) -let LF = LF | RL - -(* There should be no ordinary R or W accesses to spinlocks *) -let ALL-LOCKS = LKR | LKW | UL | LF | RU -flag ~empty [M \ IW] ; loc ; [ALL-LOCKS] as mixed-lock-accesses - -(* Link Lock-Reads to their RMW-partner Lock-Writes *) -let lk-rmw = ([LKR] ; po-loc ; [LKW]) \ (po ; po) -let rmw = rmw | lk-rmw - -(* The litmus test is invalid if an LKR/LKW event is not part of an RMW pair *) -flag ~empty LKW \ range(lk-rmw) as unpaired-LKW -flag ~empty LKR \ domain(lk-rmw) as unpaired-LKR - -(* - * An LKR must always see an unlocked value; spin_lock() calls nested - * inside a critical section (for the same lock) always deadlock. - *) -empty ([LKW] ; po-loc ; [LKR]) \ (po-loc ; [UL] ; po-loc) as lock-nest - -(* The final value of a spinlock should not be tested *) -flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final - -(* - * Put lock operations in their appropriate classes, but leave UL out of W - * until after the co relation has been generated. - *) -let R = R | LKR | LF | RU -let W = W | LKW - -let Release = Release | UL -let Acquire = Acquire | LKR - -(* Match LKW events to their corresponding UL events *) -let critical = ([LKW] ; po-loc ; [UL]) \ (po-loc ; [LKW | UL] ; po-loc) - -flag ~empty UL \ range(critical) as unmatched-unlock - -(* Allow up to one unmatched LKW per location; more must deadlock *) -let UNMATCHED-LKW = LKW \ domain(critical) -empty ([UNMATCHED-LKW] ; loc ; [UNMATCHED-LKW]) \ id as unmatched-locks - -(* rfi for LF events: link each LKW to the LF events in its critical section *) -let rfi-lf = ([LKW] ; po-loc ; [LF]) \ ([LKW] ; po-loc ; [UL] ; po-loc) - -(* rfe for LF events *) -let all-possible-rfe-lf = - (* - * Given an LF event r, compute the possible rfe edges for that event - * (all those starting from LKW events in other threads), - * and then convert that relation to a set of single-edge relations. - *) - let possible-rfe-lf r = - let pair-to-relation p = p ++ 0 - in map pair-to-relation ((LKW * {r}) & loc & ext) - (* Do this for each LF event r that isn't in rfi-lf *) - in map possible-rfe-lf (LF \ range(rfi-lf)) - -(* Generate all rf relations for LF events *) -with rfe-lf from cross(all-possible-rfe-lf) -let rf-lf = rfe-lf | rfi-lf - -(* - * RU, i.e., spin_is_locked() returning False, is slightly different. - * We rely on the memory model to rule out cases where spin_is_locked() - * within one of the lock's critical sections returns False. - *) - -(* rfi for RU events: an RU may read from the last po-previous UL *) -let rfi-ru = ([UL] ; po-loc ; [RU]) \ ([UL] ; po-loc ; [LKW] ; po-loc) - -(* rfe for RU events: an RU may read from an external UL or the initial write *) -let all-possible-rfe-ru = - let possible-rfe-ru r = - let pair-to-relation p = p ++ 0 - in map pair-to-relation (((UL | IW) * {r}) & loc & ext) - in map possible-rfe-ru RU - -(* Generate all rf relations for RU events *) -with rfe-ru from cross(all-possible-rfe-ru) -let rf-ru = rfe-ru | rfi-ru - -(* Final rf relation *) -let rf = rf | rf-lf | rf-ru - -(* Generate all co relations, including LKW events but not UL *) -let co0 = co0 | ([IW] ; loc ; [LKW]) | - (([LKW] ; loc ; [UNMATCHED-LKW]) \ [UNMATCHED-LKW]) -include "cos-opt.cat" -let W = W | UL -let M = R | W - -(* Merge UL events into co *) -let co = (co | critical | (critical^-1 ; co))+ -let coe = co & ext -let coi = co & int - -(* Merge LKR events into rf *) -let rf = rf | ([IW | UL] ; singlestep(co) ; lk-rmw^-1) -let rfe = rf & ext -let rfi = rf & int - -let fr = rf^-1 ; co -let fre = fr & ext -let fri = fr & int - -show co,rf,fr +// // SPDX-License-Identifier: GPL-2.0+ +// (* +// * Copyright (C) 2016 Luc Maranget for Inria +// * Copyright (C) 2017 Alan Stern +// *) +// +// (* +// * Generate coherence orders and handle lock operations +// * +// * Warning: spin_is_locked() crashes herd7 versions strictly before 7.48. +// * spin_is_locked() is functional from herd7 version 7.49. +// *) +// +// include "cross.cat" +// +// (* +// * The lock-related events generated by herd are as follows: +// * +// * LKR Lock-Read: the read part of a spin_lock() or successful +// * spin_trylock() read-modify-write event pair +// * LKW Lock-Write: the write part of a spin_lock() or successful +// * spin_trylock() RMW event pair +// * UL Unlock: a spin_unlock() event +// * LF Lock-Fail: a failed spin_trylock() event +// * RL Read-Locked: a spin_is_locked() event which returns True +// * RU Read-Unlocked: a spin_is_locked() event which returns False +// * +// * LKR and LKW events always come paired, like all RMW event sequences. +// * +// * LKR, LF, RL, and RU are read events; LKR has Acquire ordering. +// * LKW and UL are write events; UL has Release ordering. +// * LKW, LF, RL, and RU have no ordering properties. +// *) +// +// (* Backward compatibility *) +// let RL = try RL with emptyset +// let RU = try RU with emptyset +// +// (* Treat RL as a kind of LF: a read with no ordering properties *) +// let LF = LF | RL +// +// (* There should be no ordinary R or W accesses to spinlocks *) +// let ALL-LOCKS = LKR | LKW | UL | LF | RU +// flag ~empty [M \ IW] ; loc ; [ALL-LOCKS] as mixed-lock-accesses +// +// (* Link Lock-Reads to their RMW-partner Lock-Writes *) +// let lk-rmw = ([LKR] ; po-loc ; [LKW]) \ (po ; po) +// let rmw = rmw | lk-rmw +// +// (* The litmus test is invalid if an LKR/LKW event is not part of an RMW pair *) +// flag ~empty LKW \ range(lk-rmw) as unpaired-LKW +// flag ~empty LKR \ domain(lk-rmw) as unpaired-LKR +// +// (* +// * An LKR must always see an unlocked value; spin_lock() calls nested +// * inside a critical section (for the same lock) always deadlock. +// *) +// empty ([LKW] ; po-loc ; [LKR]) \ (po-loc ; [UL] ; po-loc) as lock-nest +// +// (* The final value of a spinlock should not be tested *) +// flag ~empty [FW] ; loc ; [ALL-LOCKS] as lock-final +// +// (* +// * Put lock operations in their appropriate classes, but leave UL out of W +// * until after the co relation has been generated. +// *) +// let R = R | LKR | LF | RU +// let W = W | LKW +// +// let Release = Release | UL +// let Acquire = Acquire | LKR +// +// (* Match LKW events to their corresponding UL events *) +// let critical = ([LKW] ; po-loc ; [UL]) \ (po-loc ; [LKW | UL] ; po-loc) +// +// flag ~empty UL \ range(critical) as unmatched-unlock +// +// (* Allow up to one unmatched LKW per location; more must deadlock *) +// let UNMATCHED-LKW = LKW \ domain(critical) +// empty ([UNMATCHED-LKW] ; loc ; [UNMATCHED-LKW]) \ id as unmatched-locks +// +// (* rfi for LF events: link each LKW to the LF events in its critical section *) +// let rfi-lf = ([LKW] ; po-loc ; [LF]) \ ([LKW] ; po-loc ; [UL] ; po-loc) +// +// (* rfe for LF events *) +// let all-possible-rfe-lf = +// (* +// * Given an LF event r, compute the possible rfe edges for that event +// * (all those starting from LKW events in other threads), +// * and then convert that relation to a set of single-edge relations. +// *) +// let possible-rfe-lf r = +// let pair-to-relation p = p ++ 0 +// in map pair-to-relation ((LKW * {r}) & loc & ext) +// (* Do this for each LF event r that isn't in rfi-lf *) +// in map possible-rfe-lf (LF \ range(rfi-lf)) +// +// (* Generate all rf relations for LF events *) +// with rfe-lf from cross(all-possible-rfe-lf) +// let rf-lf = rfe-lf | rfi-lf +// +// (* +// * RU, i.e., spin_is_locked() returning False, is slightly different. +// * We rely on the memory model to rule out cases where spin_is_locked() +// * within one of the lock's critical sections returns False. +// *) +// +// (* rfi for RU events: an RU may read from the last po-previous UL *) +// let rfi-ru = ([UL] ; po-loc ; [RU]) \ ([UL] ; po-loc ; [LKW] ; po-loc) +// +// (* rfe for RU events: an RU may read from an external UL or the initial write *) +// let all-possible-rfe-ru = +// let possible-rfe-ru r = +// let pair-to-relation p = p ++ 0 +// in map pair-to-relation (((UL | IW) * {r}) & loc & ext) +// in map possible-rfe-ru RU +// +// (* Generate all rf relations for RU events *) +// with rfe-ru from cross(all-possible-rfe-ru) +// let rf-ru = rfe-ru | rfi-ru +// +// (* Final rf relation *) +// let rf = rf | rf-lf | rf-ru +// +// (* Generate all co relations, including LKW events but not UL *) +// let co0 = co0 | ([IW] ; loc ; [LKW]) | +// (([LKW] ; loc ; [UNMATCHED-LKW]) \ [UNMATCHED-LKW]) +// include "cos-opt.cat" +// let W = W | UL +// let M = R | W +// +// (* Merge UL events into co *) +// let co = (co | critical | (critical^-1 ; co))+ +// let coe = co & ext +// let coi = co & int +// +// (* Merge LKR events into rf *) +// let rf = rf | ([IW | UL] ; singlestep(co) ; lk-rmw^-1) +// let rfe = rf & ext +// let rfi = rf & int +// +// let fr = rf^-1 ; co +// let fre = fr & ext +// let fri = fr & int +// +// show co,rf,fr + +include "basic.cat" \ No newline at end of file diff --git a/cat/power.cat b/cat/power.cat index 33e6e42e04..7711ce90a3 100644 --- a/cat/power.cat +++ b/cat/power.cat @@ -1,7 +1,7 @@ Power include "cos.cat" -include "fences.cat" +include "ppcfences.cat" (* Uniproc *) let com = rf | fr | co diff --git a/cat/ppcfences.cat b/cat/ppcfences.cat new file mode 100644 index 0000000000..8657c905c7 --- /dev/null +++ b/cat/ppcfences.cat @@ -0,0 +1,4 @@ +let sync = po;[sync];po +let isync = po;[isync];po +let lwsync = po;[lwsync];po +let ctrlisync = ctrl & isync diff --git a/cat/ptx-v6.0.cat b/cat/ptx-v6.0.cat index 85b9124ad7..8a1b3352cb 100644 --- a/cat/ptx-v6.0.cat +++ b/cat/ptx-v6.0.cat @@ -3,7 +3,7 @@ PTX // Base relations: // sr: same-scope -// sync_barrier: synchronize by barriers with same logical barrier resource (barID) +// syncbar: synchronize by barriers with same logical barrier resource (barID) // sync_fence: synchronize by morally strong fence.sc // Scope Tags: @@ -12,10 +12,14 @@ PTX // GPU: Graphics processing unit. The GPU scope is the set of all threads executing in the same cluster as the current thread. // SYS: System. The SYS scope is the set of all threads in the current program. +include "basic.cat" + (*******************) (* Auxiliaries *) (*******************) +let sync_barrier = syncbar & scta + // Explicitly add transitivity for coherence since the co in PTX is not total // and recompute fr based on the new co let co = co+ diff --git a/cat/ptx-v7.5.cat b/cat/ptx-v7.5.cat index b1701d36b9..de3f88f869 100644 --- a/cat/ptx-v7.5.cat +++ b/cat/ptx-v7.5.cat @@ -5,7 +5,7 @@ PTX // vloc: virtual address mapping to the same generic address // sr: same-scope // scta: same-cta -// sync_barrier: synchronize by barriers with same logical barrier resource (barID) +// syncbar: synchronize by barriers with same logical barrier resource (barID) // sync_fence: synchronize by morally strong fence.sc // Scope Tags: @@ -26,10 +26,14 @@ PTX // The ASPLOS'19 paper and the documentation refer to "rf | fr" (non-optional). // We follow the later. +include "basic.cat" + (*******************) (* Auxiliaries *) (*******************) +let sync_barrier = syncbar & scta + // Explicitly add transitivity for coherence since the co in PTX is not total // and recompute fr based on the new co let co = co+ diff --git a/cat/riscv-orig.cat b/cat/riscv-orig.cat index abb3999cba..266afaad2f 100644 --- a/cat/riscv-orig.cat +++ b/cat/riscv-orig.cat @@ -10,23 +10,7 @@ Partial (* Utilities *) (*************) -let fence.r.r = [R];fencerel(Fence.r.r);[R] -let fence.r.w = [R];fencerel(Fence.r.w);[W] -let fence.r.rw = [R];fencerel(Fence.r.rw);[M] -let fence.w.r = [W];fencerel(Fence.w.r);[R] -let fence.w.w = [W];fencerel(Fence.w.w);[W] -let fence.w.rw = [W];fencerel(Fence.w.rw);[M] -let fence.rw.r = [M];fencerel(Fence.rw.r);[R] -let fence.rw.w = [M];fencerel(Fence.rw.w);[W] -let fence.rw.rw = [M];fencerel(Fence.rw.rw);[M] -let fence.tso = ([W];fencerel(Fence.tso);[W]) | ([R];fencerel(Fence.tso);[M]) - -let fence = - fence.r.r | fence.r.w | fence.r.rw | - fence.w.r | fence.w.w | fence.w.rw | - fence.rw.r | fence.rw.w | fence.rw.rw | - fence.tso - +include "riscvfences.cat" let po-loc-no-w = po-loc \ (po-loc?;[W];po-loc) let rsw = rf^-1;rf diff --git a/cat/riscv.cat b/cat/riscv.cat index 495d1dec1d..8ae1aabb54 100644 --- a/cat/riscv.cat +++ b/cat/riscv.cat @@ -13,23 +13,7 @@ include "cos.cat" (* Utilities *) (*************) -let fence.r.r = [R];fencerel(Fence.r.r);[R] -let fence.r.w = [R];fencerel(Fence.r.w);[W] -let fence.r.rw = [R];fencerel(Fence.r.rw);[M] -let fence.w.r = [W];fencerel(Fence.w.r);[R] -let fence.w.w = [W];fencerel(Fence.w.w);[W] -let fence.w.rw = [W];fencerel(Fence.w.rw);[M] -let fence.rw.r = [M];fencerel(Fence.rw.r);[R] -let fence.rw.w = [M];fencerel(Fence.rw.w);[W] -let fence.rw.rw = [M];fencerel(Fence.rw.rw);[M] -let fence.tso = ([W];fencerel(Fence.tso);[W]) | ([R];fencerel(Fence.tso);[M]) - -let fence = - fence.r.r | fence.r.w | fence.r.rw | - fence.w.r | fence.w.w | fence.w.rw | - fence.rw.r | fence.rw.w | fence.rw.rw | - fence.tso - +include "riscvfences.cat" (* rdw replaces the negatively formulated relations of the original model *) let rdw = po-loc & (fre;rfe) diff --git a/cat/riscvfences.cat b/cat/riscvfences.cat new file mode 100644 index 0000000000..954d190f5a --- /dev/null +++ b/cat/riscvfences.cat @@ -0,0 +1,16 @@ +let fence.r.r = [R];fencerel(Fence.r.r);[R] +let fence.r.w = [R];fencerel(Fence.r.w);[W] +let fence.r.rw = [R];fencerel(Fence.r.rw);[M] +let fence.w.r = [W];fencerel(Fence.w.r);[R] +let fence.w.w = [W];fencerel(Fence.w.w);[W] +let fence.w.rw = [W];fencerel(Fence.w.rw);[M] +let fence.rw.r = [M];fencerel(Fence.rw.r);[R] +let fence.rw.w = [M];fencerel(Fence.rw.w);[W] +let fence.rw.rw = [M];fencerel(Fence.rw.rw);[M] +let fence.tso = ([W];fencerel(Fence.tso);[W]) | ([R];fencerel(Fence.tso);[M]) + +let fence = + fence.r.r | fence.r.w | fence.r.rw | + fence.w.r | fence.w.w | fence.w.rw | + fence.rw.r | fence.rw.w | fence.rw.rw | + fence.tso \ No newline at end of file diff --git a/cat/spirv-check.cat b/cat/spirv-check.cat index e9f53e1ed2..5fc5421641 100644 --- a/cat/spirv-check.cat +++ b/cat/spirv-check.cat @@ -64,8 +64,9 @@ let asmo = co & ((ATOM | IW) * ATOM) let fr = (rf^-1; asmo) | (([IW]; rf)^-1; ((loc;[W]) \ id)) let fre = fr & ext -let rs = [REL & ATOM]; ((asmo \ (asmo; asmo+)); [RMW])* -let hypors = [W & ATOM]; ((asmo \ (asmo; asmo+)); [RMW])* +let imm(r) = r \ (r; r+) +let rs = [REL & ATOM]; (imm(asmo); [RMW])* +let hypors = [W & ATOM]; (imm(asmo); [RMW])* // synchronizes-with is similar to C++, with an additional case for fence->cbar->cbar->fence let sw = inscope & ( @@ -132,7 +133,7 @@ let locord = loc & let w-locord = [W]; locord // visible to = location ordered W->R with no intervening write (W->W->R) -let visto = (w-locord \ (w-locord; w-locord+)); [R] +let visto = imm(w-locord); [R] (**************************) (* Sanity checks for tags *) diff --git a/cat/spirv-nochains.cat b/cat/spirv-nochains.cat index 0607eab516..779a21085a 100644 --- a/cat/spirv-nochains.cat +++ b/cat/spirv-nochains.cat @@ -64,8 +64,9 @@ let asmo = co & ((ATOM | IW) * ATOM) let fr = (rf^-1; asmo) | (([IW]; rf)^-1; ((loc;[W]) \ id)) let fre = fr & ext -let rs = [REL & ATOM]; ((asmo \ (asmo; asmo+)); [RMW])* -let hypors = [W & ATOM]; ((asmo \ (asmo; asmo+)); [RMW])* +let imm(r) = r \ (r; r+) +let rs = [REL & ATOM]; (imm(asmo); [RMW])* +let hypors = [W & ATOM]; (imm(asmo); [RMW])* // synchronizes-with is similar to C++, with an additional case for fence->cbar->cbar->fence let sw = inscope & ( diff --git a/cat/spirv.cat b/cat/spirv.cat index e94382b535..960a6eded6 100644 --- a/cat/spirv.cat +++ b/cat/spirv.cat @@ -64,8 +64,9 @@ let asmo = co & ((ATOM | IW) * ATOM) let fr = (rf^-1; asmo) | (([IW]; rf)^-1; ((loc;[W]) \ id)) let fre = fr & ext -let rs = [REL & ATOM]; ((asmo \ (asmo; asmo+)); [RMW])* -let hypors = [W & ATOM]; ((asmo \ (asmo; asmo+)); [RMW])* +let imm(r) = r \ (r; r+) +let rs = [REL & ATOM]; (imm(asmo); [RMW])* +let hypors = [W & ATOM]; (imm(asmo); [RMW])* // synchronizes-with is similar to C++, with an additional case for fence->cbar->cbar->fence let sw = inscope & ( diff --git a/cat/tso.cat b/cat/tso.cat index ee06e5cc5a..9f81377cd0 100644 --- a/cat/tso.cat +++ b/cat/tso.cat @@ -1,6 +1,7 @@ "X86 TSO" + include "cos.cat" -include "fences.cat" +include "x86fences.cat" include "filters.cat" (* All communication relations *) diff --git a/cat/vmm.cat b/cat/vmm.cat index d97919cc45..f6dd21e5ea 100644 --- a/cat/vmm.cat +++ b/cat/vmm.cat @@ -55,12 +55,8 @@ let ext = ext & ((~IW) * M) let int = int | (IW * M) -let rfe = rf & ext -let coe = co & ext -let fre = fr & ext -let rfi = rf & int -let coi = co & int -let fri = fr & int + +include "basic.cat" (** Atomicity **) empty rmw & (fre;coe) diff --git a/cat/x86fences.cat b/cat/x86fences.cat new file mode 100644 index 0000000000..4116b06262 --- /dev/null +++ b/cat/x86fences.cat @@ -0,0 +1 @@ +let mfence = po;[mfence];po \ No newline at end of file diff --git a/dartagnan/src/main/antlr4/Cat.g4 b/dartagnan/src/main/antlr4/Cat.g4 index c3e268437c..84b4323be7 100755 --- a/dartagnan/src/main/antlr4/Cat.g4 +++ b/dartagnan/src/main/antlr4/Cat.g4 @@ -5,11 +5,12 @@ import com.dat3m.dartagnan.wmm.axiom.*; } mcm - : (NAME)? definition+ EOF + : (NAME)? (QUOTED_STRING)? (definition | include)+ EOF ; definition : axiomDefinition + | letFuncDefinition | letDefinition | letRecDefinition ; @@ -20,6 +21,10 @@ axiomDefinition locals [Class cls] | (flag = FLAG)? (negate = NOT)? EMPTY { $cls = Emptiness.class; } e = expression (AS NAME)? ; +letFuncDefinition + : LET (fname = NAME) LPAR params = parameterList RPAR EQ e = expression + ; + letDefinition : LET n = NAME EQ e = expression ; @@ -46,10 +51,22 @@ expression | LBRAC DOMAIN LPAR e = expression RPAR RBRAC # exprDomainIdentity | LBRAC RANGE LPAR e = expression RPAR RBRAC # exprRangeIdentity | (TOID LPAR e = expression RPAR | LBRAC e = expression RBRAC) # exprIdentity - | FENCEREL LPAR e = expression RPAR # exprFencerel | LPAR e = expression RPAR # expr | n = NAME # exprBasic | call = NEW LPAR RPAR # exprNew + | call = NAME LPAR args = argumentList RPAR # exprCall + ; + +include + : 'include' path = QUOTED_STRING + ; + +parameterList + : (NAME (COMMA NAME)*) + ; + +argumentList + : expression (COMMA expression)* ; LET : 'let'; @@ -78,14 +95,16 @@ LPAR : '('; RPAR : ')'; LBRAC : '['; RBRAC : ']'; +COMMA : ','; -FENCEREL : 'fencerel'; DOMAIN : 'domain'; RANGE : 'range'; NEW : 'new'; FLAG : 'flag'; +QUOTED_STRING : '"' .*? '"'; + NAME : [A-Za-z0-9\-_.]+; LINE_COMMENT @@ -102,13 +121,3 @@ WS : [ \t\r\n]+ -> skip ; - -INCLUDE - : 'include "' .*? '"' - -> skip - ; - -MODELNAME - : '"' .*? '"' - -> skip - ; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 11d0695819..6709bdb8df 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -52,6 +52,7 @@ import java.io.FileReader; import java.io.IOException; import java.math.BigInteger; +import java.nio.file.Path; import java.util.*; import static com.dat3m.dartagnan.GlobalSettings.getOrCreateOutputDirectory; @@ -112,19 +113,20 @@ public static void main(String[] args) throws Exception { File fileProgram = new File(Arrays.stream(args).filter(a -> supportedFormats.stream().anyMatch(a::endsWith)) .findFirst() .orElseThrow(() -> new IllegalArgumentException("Input program not given or format not recognized"))); - logger.info("Program path: " + fileProgram); + logger.info("Program path: {}", fileProgram); File fileModel = new File(Arrays.stream(args).filter(a -> a.endsWith(".cat")).findFirst() .orElseThrow(() -> new IllegalArgumentException("CAT model not given or format not recognized"))); - logger.info("CAT file path: " + fileModel); + logger.info("CAT file path: {}", fileModel); - Wmm mcm = new ParserCat().parse(fileModel); + + Wmm mcm = new ParserCat(Path.of(o.getCatIncludePath())).parse(fileModel); Program p = new ProgramParser().parse(fileProgram); EnumSet properties = o.getProperty(); WitnessGraph witness = new WitnessGraph(); if (o.runValidator()) { - logger.info("Witness path: " + o.getWitnessPath()); + logger.info("Witness path: {}", o.getWitnessPath()); witness = new ParserWitness().parse(new File(o.getWitnessPath())); } @@ -166,8 +168,7 @@ public static void main(String[] args) throws Exception { sdm.getNotifier(), o.getSolver()); ProverWithTracker prover = new ProverWithTracker(ctx, - o.getDumpSmtLib() ? - System.getenv("DAT3M_OUTPUT") + String.format("/%s.smt2", p.getName()) : "", + o.getDumpSmtLib() ? GlobalSettings.getOutputDirectory() + String.format("/%s.smt2", p.getName()) : "", ProverOptions.GENERATE_MODELS)) { ModelChecker modelChecker; if (properties.contains(DATARACEFREEDOM)) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java b/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java index 8d7d52b1fb..6e36bebf24 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/GlobalSettings.java @@ -59,6 +59,12 @@ public static String getHomeDirectory() { return env; } + public static String getCatDirectory() { + String env = System.getenv("DAT3M_HOME"); + env = env == null ? "" : env; + return env + "/cat"; + } + public static String getOrCreateOutputDirectory() throws IOException { String path = getOutputDirectory(); Files.createDirectories(Paths.get(path)); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java index b4aeef42c3..7fbbae45aa 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java @@ -13,6 +13,7 @@ public class OptionNames { public static final String COVERAGE = "coverage"; public static final String WITNESS = "witness"; public static final String SMTLIB2 = "smtlib2"; + public static final String CAT_INCLUDE = "cat.include"; // Modeling Options public static final String PROGRESSMODEL = "modeling.progress"; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java index 47c66da65b..1034609ac1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/WmmEncoder.java @@ -356,29 +356,6 @@ public Void visitInverse(Inverse inv) { return null; } - @Override - public Void visitFences(Fences fence) { - final Relation rel = fence.getDefinedRelation(); - final Filter fenceSet = fence.getFilter(); - EventGraph mustSet = ra.getKnowledge(rel).getMustSet(); - List fences = program.getThreadEvents().stream().filter(fenceSet::apply).toList(); - EncodingContext.EdgeEncoder encoder = context.edge(rel); - encodeSets.get(rel).apply((e1, e2) -> { - BooleanFormula orClause; - if (mustSet.contains(e1, e2)) { - orClause = bmgr.makeTrue(); - } else { - orClause = fences.stream() - .filter(f -> e1.getGlobalId() < f.getGlobalId() && f.getGlobalId() < e2.getGlobalId()) - .map(context::execution).reduce(bmgr.makeFalse(), bmgr::or); - } - enc.add(bmgr.equivalence( - encoder.encode(e1, e2), - bmgr.and(execution(e1, e2), orClause))); - }); - return null; - } - @Override public Void visitInternalDataDependency(DirectDataDependency idd) { return visitDirectDependency(idd.getDefinedRelation()); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/ParserCat.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/ParserCat.java index 753625ce88..33f7315286 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/ParserCat.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/ParserCat.java @@ -1,17 +1,29 @@ package com.dat3m.dartagnan.parsers.cat; +import com.dat3m.dartagnan.GlobalSettings; +import com.dat3m.dartagnan.exception.AbortErrorListener; import com.dat3m.dartagnan.parsers.CatLexer; import com.dat3m.dartagnan.parsers.CatParser; -import com.dat3m.dartagnan.exception.AbortErrorListener; import com.dat3m.dartagnan.wmm.Wmm; import org.antlr.v4.runtime.*; import java.io.File; import java.io.FileInputStream; import java.io.IOException; +import java.nio.file.Path; public class ParserCat { + private final Path includePath; + + public ParserCat() { + includePath = Path.of(GlobalSettings.getCatDirectory()); + } + + public ParserCat(Path includePath) { + this.includePath = includePath; + } + public Wmm parse(File file) throws IOException { try (FileInputStream stream = new FileInputStream(file)) { return parse(CharStreams.fromStream(stream)); @@ -32,6 +44,6 @@ private Wmm parse(CharStream charStream){ parser.addErrorListener(new AbortErrorListener()); parser.addErrorListener(new DiagnosticErrorListener(true)); ParserRuleContext parserEntryPoint = parser.mcm(); - return (Wmm) parserEntryPoint.accept(new VisitorBase()); + return (Wmm) parserEntryPoint.accept(new VisitorCat(includePath)); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorBase.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java similarity index 73% rename from dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorBase.java rename to dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java index 400c120d7a..be11ef0c07 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorBase.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/cat/VisitorCat.java @@ -1,8 +1,11 @@ package com.dat3m.dartagnan.parsers.cat; +import com.dat3m.dartagnan.exception.AbortErrorListener; import com.dat3m.dartagnan.exception.MalformedMemoryModelException; import com.dat3m.dartagnan.exception.ParsingException; import com.dat3m.dartagnan.parsers.CatBaseVisitor; +import com.dat3m.dartagnan.parsers.CatLexer; +import com.dat3m.dartagnan.parsers.CatParser; import com.dat3m.dartagnan.parsers.CatParser.*; import com.dat3m.dartagnan.program.filter.Filter; import com.dat3m.dartagnan.wmm.Definition; @@ -11,30 +14,53 @@ import com.dat3m.dartagnan.wmm.Wmm; import com.dat3m.dartagnan.wmm.axiom.Axiom; import com.dat3m.dartagnan.wmm.definition.*; +import com.google.common.collect.ImmutableMap; +import org.antlr.v4.runtime.*; +import org.apache.logging.log4j.LogManager; +import org.apache.logging.log4j.Logger; +import java.io.IOException; import java.lang.reflect.Constructor; import java.lang.reflect.InvocationTargetException; -import java.util.Arrays; -import java.util.HashMap; -import java.util.Map; -import java.util.Optional; +import java.nio.file.Files; +import java.nio.file.Path; +import java.util.*; +import java.util.stream.Collectors; import static com.dat3m.dartagnan.program.event.Tag.VISIBLE; import static com.dat3m.dartagnan.wmm.RelationNameRepository.ID; -class VisitorBase extends CatBaseVisitor { +class VisitorCat extends CatBaseVisitor { + + private static final Logger logger = LogManager.getLogger(VisitorCat.class); + + // The directory path used to resolve include statements. + private final Path includePath; private final Wmm wmm; - // Maps names used on the lhs of definitions ("let name = relexpr") to the - // predicate they identify (either a Relation or a Filter). - private final Map namespace = new HashMap<>(); + // Maps names used on the lhs of definitions ("let name = relexpr" or "let name(params) = relexpr") to the + // predicate (either a Relation or a Filter) or the function (FuncDefinition) they identify + private Map namespace = new HashMap<>(); // Counts the number of occurrences of a name on the lhs of a definition // This is used to give proper names to re-definitions private final Map nameOccurrenceCounter = new HashMap<>(); // Used to handle recursive definitions properly private Relation relationToBeDefined; - VisitorBase() { + private record FuncDefinition(String name, List params, String expression, + Map capturedNamespace) { + @Override + public String toString() { + return String.format("%s%s := %s", + name, + params.stream().collect(Collectors.joining(", ", "(", ")")), + expression + ); + } + } + + VisitorCat(Path includePath) { + this.includePath = includePath; this.wmm = new Wmm(); } @@ -44,6 +70,35 @@ public Object visitMcm(McmContext ctx) { return wmm; } + @Override + public Object visitLetFuncDefinition(LetFuncDefinitionContext ctx) { + final String fname = ctx.fname.getText(); + final List params = ctx.params.NAME().stream().map(Object::toString).toList(); + final String expression = ctx.expression().getText(); + final Map capturedNamespace = ImmutableMap.copyOf(namespace); + + final FuncDefinition definition = new FuncDefinition(fname, params, expression, capturedNamespace); + namespace.put(fname, definition); + return null; + } + + @Override + public Object visitInclude(IncludeContext ctx) { + final String fileName = ctx.path.getText().substring(1, ctx.path.getText().length() - 1); + final Path filePath = includePath.resolve(Path.of(fileName)); + if (!Files.exists(filePath)) { + logger.warn("Included file '{}' not found. Skipped inclusion.", filePath); + return null; + } + + try { + final CatParser parser = getParser(CharStreams.fromPath(filePath)); + return parser.mcm().accept(this); + } catch (IOException e) { + throw new ParsingException(String.format("Error parsing file '%s'", filePath), e); + } + } + @Override public Void visitAxiomDefinition(AxiomDefinitionContext ctx) { try { @@ -154,6 +209,34 @@ public Object visitExprBasic(ExprBasicContext ctx) { return predicate; } + @Override + public Object visitExprCall(ExprCallContext ctx) { + final String calledFunc = ctx.call.getText(); + if (!(namespace.get(calledFunc) instanceof FuncDefinition funcDef)) { + final String error = String.format("Invalid call %s: %s is undefined or no function.", ctx.getText(), calledFunc); + throw new ParsingException(error); + } + + final List args = ctx.args.expression(); + if (args.size() != funcDef.params().size()) { + final String error = String.format("Invalid call %s to function %s: wrong number of arguments.", + ctx.getText(), funcDef); + throw new ParsingException(error); + } + final List arguments = ctx.args.expression().stream().map(e -> e.accept(this)).toList(); + final Map functionNamespace = new HashMap<>(funcDef.capturedNamespace()); + for (int i = 0; i < arguments.size(); i++) { + functionNamespace.put(funcDef.params.get(i), arguments.get(i)); + } + + final Map curNamespace = namespace; + namespace = functionNamespace; + final CatParser parser = getParser(CharStreams.fromString(funcDef.expression)); + Object result = parser.expression().accept(this); + namespace = curNamespace; + return result; + } + @Override public Object visitExprIntersection(ExprIntersectionContext c) { Optional defRel = getAndResetRelationToBeDefined(); @@ -271,14 +354,6 @@ public Relation visitExprCartesian(ExprCartesianContext c) { return addDefinition(new CartesianProduct(r0, s1, s2)); } - @Override - public Relation visitExprFencerel(ExprFencerelContext ctx) { - checkNoRecursion(ctx); - Relation r0 = wmm.newRelation(); - Filter s1 = parseAsFilter(ctx.e); - return addDefinition(new Fences(r0, s1)); - } - // ============================ Utility ============================ private Relation addDefinition(Definition definition) { @@ -322,5 +397,17 @@ private static Filter parseAsFilter(Object o, ExpressionContext t) { } throw new ParsingException("Expected set, got " + o.getClass().getSimpleName() + " " + o + " from expression " + t.getText()); } + + private static CatParser getParser(CharStream input) { + final Lexer lexer = new CatLexer(input); + lexer.addErrorListener(new AbortErrorListener()); + lexer.addErrorListener(new DiagnosticErrorListener(true)); + final CommonTokenStream tokenStream = new CommonTokenStream(lexer); + + final CatParser parser = new CatParser(tokenStream); + parser.addErrorListener(new AbortErrorListener()); + parser.addErrorListener(new DiagnosticErrorListener(true)); + return parser; + } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java index 09c8c3933f..a26bda4444 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPPC.java @@ -19,7 +19,7 @@ import java.util.HashMap; import java.util.Map; -import static com.dat3m.dartagnan.wmm.RelationNameRepository.*; +import static com.dat3m.dartagnan.program.event.FenceNameRepository.*; public class VisitorLitmusPPC extends LitmusPPCBaseVisitor { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusX86.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusX86.java index e604b6bf65..dfd674dbfb 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusX86.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusX86.java @@ -15,7 +15,7 @@ import com.dat3m.dartagnan.program.memory.MemoryObject; import com.google.common.collect.ImmutableSet; -import static com.dat3m.dartagnan.wmm.RelationNameRepository.MFENCE; +import static com.dat3m.dartagnan.program.event.FenceNameRepository.*; public class VisitorLitmusX86 extends LitmusX86BaseVisitor { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java index cc796e6417..add6cc5009 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/EventFactory.java @@ -45,7 +45,7 @@ import java.util.*; import java.util.stream.Collectors; -import static com.dat3m.dartagnan.wmm.RelationNameRepository.*; +import static com.dat3m.dartagnan.program.event.FenceNameRepository.*; public class EventFactory { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/FenceNameRepository.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/FenceNameRepository.java new file mode 100644 index 0000000000..5f635a8d5b --- /dev/null +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/event/FenceNameRepository.java @@ -0,0 +1,10 @@ +package com.dat3m.dartagnan.program.event; + +public class FenceNameRepository { + + public static final String MFENCE = "mfence"; + public static final String SYNC = "sync"; + public static final String ISYNC = "isync"; + public static final String LWSYNC = "lwsync"; + +} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java index 3c9abcdd54..a6981cbb03 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/solver/caat4wmm/ExecutionGraph.java @@ -258,8 +258,6 @@ private RelationGraph createGraphFromRelation(Relation rel) { graph = new ExternalGraph(); } else if (relClass == Internal.class) { graph = new InternalGraph(); - } else if (relClass == Fences.class) { - throw new UnsupportedOperationException("fencerel is not supported in CAAT."); } else if (relClass == SetIdentity.class) { SetPredicate set = getOrCreateSetFromFilter(((SetIdentity) rel.getDefinition()).getFilter()); graph = new SetIdentityGraph(set); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java index c121bd263d..176c97689d 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/options/BaseOptions.java @@ -1,5 +1,6 @@ package com.dat3m.dartagnan.utils.options; +import com.dat3m.dartagnan.GlobalSettings; import com.dat3m.dartagnan.configuration.Method; import com.dat3m.dartagnan.configuration.ProgressModel; import com.dat3m.dartagnan.configuration.Property; @@ -107,4 +108,14 @@ public WitnessType getWitnessType() { public boolean getDumpSmtLib() { return smtlib; } + + @Option( + name = CAT_INCLUDE, + description = "The directory used to resolve cat include statements. Defaults to $DAT3M_HOME/cat." + ) + private String catIncludePath = GlobalSettings.getCatDirectory(); + + public String getCatIncludePath() { + return catIncludePath; + } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java index f1b70d4c45..6aa6619b73 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java @@ -14,6 +14,8 @@ import com.dat3m.dartagnan.program.event.core.MemoryCoreEvent; import com.dat3m.dartagnan.program.event.metadata.OriginalId; import com.dat3m.dartagnan.program.event.metadata.SourceLocation; +import com.dat3m.dartagnan.program.filter.Filter; +import com.dat3m.dartagnan.program.event.Tag; import com.dat3m.dartagnan.solver.caat.CAATSolver; import com.dat3m.dartagnan.solver.caat4wmm.RefinementModel; import com.dat3m.dartagnan.solver.caat4wmm.Refiner; @@ -81,6 +83,11 @@ public class RefinementSolver extends ModelChecker { private static final Logger logger = LogManager.getLogger(RefinementSolver.class); + private static final String FR = "fr"; + private static final String COE = "coe"; + private static final String FRE = "fre"; + private static final String POLOC = "po-loc"; + // ================================================================================================================ // Configuration @@ -510,47 +517,62 @@ private static RefinementModel generateRefinementModel(Wmm original) { if (name.equals(DATA) || name.equals(CTRL) || name.equals(ADDR) || isUnknownDefinitionForCAAT(def)) { constraintsToCut.add(c); } - } else if (c instanceof Definition def && def instanceof Fences) { - // (iii) continued: fencerel(F) is unsupported in CAAT. - // It should get rewritten to "po;[F];po" by our passes, - // but if it was not, we cut it instead. - constraintsToCut.add(c); } } return RefinementModel.fromCut(Cut.computeInducedCut(original, constraintsToCut)); } - private static void addBiases(Wmm memoryModel, EnumSet biases) { - // FIXME: This can (in theory) add redundant intermediate relations and/or constraints that - // already exist in the model. - final Relation rf = memoryModel.getRelation(RF); + private static void addBiases(Wmm wmm, EnumSet biases) { + + // Base relations + final Relation rf = wmm.getRelation(RF); + final Relation co = wmm.getOrCreatePredefinedRelation(CO); + final Relation loc = wmm.getOrCreatePredefinedRelation(LOC); + final Relation po = wmm.getOrCreatePredefinedRelation(PO); + final Relation ext = wmm.getOrCreatePredefinedRelation(EXT); + final Relation rmw = wmm.getOrCreatePredefinedRelation(RMW); + + // rf^-1;co + final Relation rfinv = wmm.addDefinition(new Inverse(wmm.newRelation(), rf)); + final Relation frStandard = wmm.addDefinition(new Composition(wmm.newRelation(), rfinv, co)); + + // ([R] \ [range(rf)]);loc;[W] + final Relation reads = wmm.addDefinition(new SetIdentity(wmm.newRelation(), wmm.getFilter(Tag.READ))); + final Relation rfRange = wmm.addDefinition(new RangeIdentity(wmm.newRelation(), rf)); + final Relation writes = wmm.addDefinition(new SetIdentity(wmm.newRelation(), Filter.byTag(Tag.WRITE))); + final Relation ur = wmm.addDefinition(new Difference(wmm.newRelation(), reads, rfRange)); + final Relation urloc = wmm.addDefinition(new Composition(wmm.newRelation(), ur, loc)); + final Relation urlocwrites = wmm.addDefinition(new Composition(wmm.newRelation(), urloc, writes)); + + // let fr = rf^-1;co | ([R] \ [range(rf)]);loc;[W] + final Relation fr = wmm.addDefinition(new Union(wmm.newRelation(), frStandard, urlocwrites)); + if (biases.contains(Baseline.UNIPROC)) { // ---- acyclic(po-loc | com) ---- - memoryModel.addConstraint(new Acyclicity(memoryModel.addDefinition(new Union(memoryModel.newRelation(), - memoryModel.getOrCreatePredefinedRelation(POLOC), - rf, - memoryModel.getOrCreatePredefinedRelation(CO), - memoryModel.getOrCreatePredefinedRelation(FR) + wmm.addConstraint(new Acyclicity(wmm.addDefinition(new Union(wmm.newRelation(), + wmm.addDefinition(new Intersection(wmm.newRelation(), po, loc)), + rf, + co, + fr )))); } if (biases.contains(Baseline.NO_OOTA)) { // ---- acyclic (dep | rf) ---- - memoryModel.addConstraint(new Acyclicity(memoryModel.addDefinition(new Union(memoryModel.newRelation(), - memoryModel.getOrCreatePredefinedRelation(CTRL), - memoryModel.getOrCreatePredefinedRelation(DATA), - memoryModel.getOrCreatePredefinedRelation(ADDR), - rf) + wmm.addConstraint(new Acyclicity(wmm.addDefinition(new Union(wmm.newRelation(), + wmm.getOrCreatePredefinedRelation(CTRL), + wmm.getOrCreatePredefinedRelation(DATA), + wmm.getOrCreatePredefinedRelation(ADDR), + rf) ))); } if (biases.contains(Baseline.ATOMIC_RMW)) { // ---- empty (rmw & fre;coe) ---- - Relation rmw = memoryModel.getOrCreatePredefinedRelation(RMW); - Relation coe = memoryModel.getOrCreatePredefinedRelation(COE); - Relation fre = memoryModel.getOrCreatePredefinedRelation(FRE); - Relation frecoe = memoryModel.addDefinition(new Composition(memoryModel.newRelation(), fre, coe)); - Relation rmwANDfrecoe = memoryModel.addDefinition(new Intersection(memoryModel.newRelation(), rmw, frecoe)); - memoryModel.addConstraint(new Emptiness(rmwANDfrecoe)); + Relation coe = wmm.addDefinition(new Intersection(wmm.newRelation(), co, ext)); + Relation fre = wmm.addDefinition(new Intersection(wmm.newRelation(), fr, ext)); + Relation frecoe = wmm.addDefinition(new Composition(wmm.newRelation(), fre, coe)); + Relation rmwANDfrecoe = wmm.addDefinition(new Intersection(wmm.newRelation(), rmw, frecoe)); + wmm.addConstraint(new Emptiness(rmwANDfrecoe)); } } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java index 4c5ef52794..73929a897f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Constraint.java @@ -70,7 +70,6 @@ default T visitConstraint(Constraint constraint) { // These three are semi-derived (they are derived from sets/filters and not from relations). default T visitSetIdentity(SetIdentity def) { return visitDefinition(def); } default T visitProduct(CartesianProduct def) { return visitDefinition(def); } - default T visitFences(Fences fence) { return visitDefinition(fence); } // Base default T visitUndefined(Definition.Undefined def) { return visitDefinition(def); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/RelationNameRepository.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/RelationNameRepository.java index 6c865ec9f8..72b4f3e1e6 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/RelationNameRepository.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/RelationNameRepository.java @@ -15,30 +15,10 @@ public class RelationNameRepository { public static final String RF = "rf"; public static final String RMW = "rmw"; public static final String CRIT = "rcu-rscs"; - public static final String IDD = "idd"; - public static final String ADDRDIRECT = "addrDirect"; - public static final String CTRLDIRECT = "ctrlDirect"; public static final String EMPTY = "0"; - public static final String FR = "fr"; - public static final String IDDTRANS = "idd^+"; public static final String DATA = "data"; public static final String ADDR = "addr"; public static final String CTRL = "ctrl"; - public static final String POLOC = "po-loc"; - public static final String RFE = "rfe"; - public static final String RFI = "rfi"; - public static final String COE = "coe"; - public static final String COI = "coi"; - public static final String FRE = "fre"; - public static final String FRI = "fri"; - public static final String MFENCE = "mfence"; - public static final String ISH = "ish"; - public static final String ISB = "isb"; - public static final String SYNC = "sync"; - public static final String ISYNC = "isync"; - public static final String LWSYNC = "lwsync"; - public static final String CTRLISYNC = "ctrlisync"; - public static final String CTRLISB = "ctrlisb"; public static final String CASDEP = "casdep"; public static final String SR = "sr"; public static final String SCTA = "scta"; // same-cta, the same as same_block_r in alloy @@ -46,10 +26,14 @@ public class RelationNameRepository { public static final String SWG = "swg"; public static final String SQF = "sqf"; public static final String SSW = "ssw"; - public static final String SYNC_BARRIER = "sync_barrier"; public static final String SYNC_FENCE = "sync_fence"; public static final String SYNCBAR = "syncbar"; public static final String VLOC = "vloc"; + // private relations, not to be exposed in cat + public static final String IDD = "__idd"; + public static final String ADDRDIRECT = "__addrDirect"; + public static final String CTRLDIRECT = "__ctrlDirect"; + public static final String IDDTRANS = "__iddTrans"; public static final ImmutableSet RELATION_NAMES; diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java index d72941cc91..3cd185fd67 100755 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/Wmm.java @@ -202,24 +202,6 @@ private Relation makePredefinedRelation(String name) { case ADDRDIRECT -> new DirectAddressDependency(r); case CTRLDIRECT -> new DirectControlDependency(r); case EMPTY -> new Empty(r); - case FR -> { - // rf^-1;co - final Relation rfinv = addDefinition(new Inverse(newRelation(), getOrCreatePredefinedRelation(RF))); - final Relation co = getOrCreatePredefinedRelation(CO); - final Relation frStandard = addDefinition(composition(newRelation(), rfinv, co)); - - // ([R] \ [range(rf)]);loc;[W] - final Relation reads = addDefinition(new SetIdentity(newRelation(), getFilter(Tag.READ))); - final Relation rfRange = addDefinition(new RangeIdentity(newRelation(), getOrCreatePredefinedRelation(RF))); - final Relation loc = getOrCreatePredefinedRelation(LOC); - final Relation writes = addDefinition(new SetIdentity(newRelation(), Filter.byTag(Tag.WRITE))); - final Relation ur = addDefinition(new Difference(newRelation(), reads, rfRange)); - final Relation urloc = addDefinition(composition(newRelation(), ur, loc)); - final Relation urlocwrites = addDefinition(composition(newRelation(), urloc, writes)); - - // let fr = rf^-1;co | ([R] \ [range(rf)]);loc;[W] - yield union(r, frStandard, urlocwrites); - } case IDDTRANS -> new TransitiveClosure(r, getOrCreatePredefinedRelation(IDD)); case DATA -> intersection(r, getOrCreatePredefinedRelation(IDDTRANS), @@ -238,21 +220,6 @@ private Relation makePredefinedRelation(String name) { Relation mv = addDefinition(product(newRelation(), Tag.MEMORY, Tag.VISIBLE)); yield intersection(r, comp, mv); } - case POLOC -> intersection(r, getOrCreatePredefinedRelation(PO), getOrCreatePredefinedRelation(LOC)); - case RFE -> intersection(r, getOrCreatePredefinedRelation(RF), getOrCreatePredefinedRelation(EXT)); - case RFI -> intersection(r, getOrCreatePredefinedRelation(RF), getOrCreatePredefinedRelation(INT)); - case COE -> intersection(r, getOrCreatePredefinedRelation(CO), getOrCreatePredefinedRelation(EXT)); - case COI -> intersection(r, getOrCreatePredefinedRelation(CO), getOrCreatePredefinedRelation(INT)); - case FRE -> intersection(r, getOrCreatePredefinedRelation(FR), getOrCreatePredefinedRelation(EXT)); - case FRI -> intersection(r, getOrCreatePredefinedRelation(FR), getOrCreatePredefinedRelation(INT)); - case MFENCE -> fence(r, MFENCE); - case ISH -> fence(r, ISH); - case ISB -> fence(r, ISB); - case SYNC -> fence(r, SYNC); - case ISYNC -> fence(r, ISYNC); - case LWSYNC -> fence(r, LWSYNC); - case CTRLISYNC -> intersection(r, getOrCreatePredefinedRelation(CTRL), getOrCreatePredefinedRelation(ISYNC)); - case CTRLISB -> intersection(r, getOrCreatePredefinedRelation(CTRL), getOrCreatePredefinedRelation(ISB)); case SR -> new SameScope(r); case SCTA -> new SameScope(r, Tag.PTX.CTA); case SSG -> new SameScope(r, Tag.Vulkan.SUB_GROUP); @@ -260,11 +227,10 @@ private Relation makePredefinedRelation(String name) { case SQF -> new SameScope(r, Tag.Vulkan.QUEUE_FAMILY); case SSW -> new SyncWith(r); case SYNCBAR -> new SyncBar(r); - case SYNC_BARRIER -> intersection(r, getOrCreatePredefinedRelation(SYNCBAR), getOrCreatePredefinedRelation(SCTA)); case SYNC_FENCE -> new SyncFence(r); case VLOC -> new SameVirtualLocation(r); default -> - throw new RuntimeException(name + "is part of RelationNameRepository but it has no associated relation."); + throw new RuntimeException(name + " is part of RelationNameRepository but it has no associated relation."); }; return addDefinition(def); } @@ -281,10 +247,6 @@ private Definition composition(Relation r0, Relation r1, Relation r2) { return new Composition(r0, r1, r2); } - private Definition fence(Relation r0, String name) { - return new Fences(r0, Filter.byTag(name)); - } - private Definition product(Relation r0, String tag1, String tag2) { return new CartesianProduct(r0, Filter.byTag(tag1), Filter.byTag(tag2)); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java index 2f9ec76059..8ef721f364 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java @@ -607,39 +607,6 @@ public Knowledge visitInternalDataDependency(DirectDataDependency idd) { return computeInternalDependencies(EnumSet.of(DATA, CTRL, OTHER)); } - @Override - public Knowledge visitFences(Fences fenceDef) { - final Filter fence = fenceDef.getFilter(); - EventGraph may = new EventGraph(); - EventGraph must = new EventGraph(); - for (Thread t : program.getThreads()) { - List events = visibleEvents(t); - int end = events.size(); - for (int i = 0; i < end; i++) { - Event f = events.get(i); - if (!fence.apply(f)) { - continue; - } - for (Event x : events.subList(0, i)) { - if (exec.areMutuallyExclusive(x, f)) { - continue; - } - boolean implies = exec.isImplied(x, f); - for (Event y : events.subList(i + 1, end)) { - if (exec.areMutuallyExclusive(x, y) || exec.areMutuallyExclusive(f, y)) { - continue; - } - may.add(x, y); - if (implies || exec.isImplied(y, f)) { - must.add(x, y); - } - } - } - } - } - return new Knowledge(may, must); - } - @Override public Knowledge visitCASDependency(CASDependency casDep) { EventGraph must = new EventGraph(); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Fences.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Fences.java deleted file mode 100644 index 1d77cc7514..0000000000 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/Fences.java +++ /dev/null @@ -1,23 +0,0 @@ -package com.dat3m.dartagnan.wmm.definition; - -import com.dat3m.dartagnan.program.filter.Filter; -import com.dat3m.dartagnan.wmm.Definition; -import com.dat3m.dartagnan.wmm.Relation; - -public class Fences extends Definition { - - private final Filter filter; - - public Fences(Relation r0, Filter s1) { - super(r0, "fencerel(" + s1 + ")"); - filter = s1; - } - - public Filter getFilter() { return filter; } - - @Override - public T accept(Visitor v) { - return v.visitFences(this); - } - -} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncBar.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncBar.java index fa2ef35884..1167a8bf64 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncBar.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/definition/SyncBar.java @@ -7,7 +7,7 @@ public class SyncBar extends Definition { public SyncBar(Relation r) { - super(r, RelationNameRepository.SYNC_BARRIER); + super(r, RelationNameRepository.SYNCBAR); } @Override public T accept(Visitor v) { diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/MergeEquivalentRelations.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/MergeEquivalentRelations.java index 3b19b0e5ab..f9ca0337ab 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/MergeEquivalentRelations.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/MergeEquivalentRelations.java @@ -85,9 +85,6 @@ private boolean areEquivalent(Relation r1, Relation r2) { if (def1 instanceof CartesianProduct p1 && def2 instanceof CartesianProduct p2) { return p1.getFirstFilter().equals(p2.getFirstFilter()) && p1.getSecondFilter().equals(p2.getSecondFilter()); } - if (def1 instanceof Fences f1 && def2 instanceof Fences f2) { - return f1.getFilter().equals(f2.getFilter()); - } if (def1 instanceof SameScope s1 && def2 instanceof SameScope s2) { return Objects.equals(s1.getSpecificScope(), s2.getSpecificScope()); } diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/NormalizeFenceRelations.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/NormalizeFenceRelations.java deleted file mode 100644 index a3f42cde5d..0000000000 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/NormalizeFenceRelations.java +++ /dev/null @@ -1,37 +0,0 @@ -package com.dat3m.dartagnan.wmm.processing; - -import com.dat3m.dartagnan.wmm.Relation; -import com.dat3m.dartagnan.wmm.RelationNameRepository; -import com.dat3m.dartagnan.wmm.Wmm; -import com.dat3m.dartagnan.wmm.definition.Composition; -import com.dat3m.dartagnan.wmm.definition.Fences; -import com.dat3m.dartagnan.wmm.definition.SetIdentity; - -import java.util.List; - -/* - This pass replaces "fencerel(F)" by "po;[F];po" - */ -public class NormalizeFenceRelations implements WmmProcessor { - - private NormalizeFenceRelations() { - } - - public static NormalizeFenceRelations newInstance() { - return new NormalizeFenceRelations(); - } - - @Override - public void run(Wmm wmm) { - final Relation po = wmm.getRelation(RelationNameRepository.PO); - - for (Relation rel : List.copyOf(wmm.getRelations())) { - if (rel.getDefinition() instanceof Fences fence) { - final Relation fenceId = wmm.addDefinition(new SetIdentity(wmm.newRelation(), fence.getFilter())); - final Relation intermediate = wmm.addDefinition(new Composition(wmm.newRelation(), po, fenceId)); - wmm.removeDefinition(rel); - wmm.addDefinition(new Composition(rel, intermediate, po)); - } - } - } -} diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/WmmProcessingManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/WmmProcessingManager.java index 58e1974ced..f614f31079 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/WmmProcessingManager.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/processing/WmmProcessingManager.java @@ -26,7 +26,6 @@ public class WmmProcessingManager implements WmmProcessor { private WmmProcessingManager(Configuration config) throws InvalidConfigurationException { config.inject(this); processors.addAll(Arrays.asList( - NormalizeFenceRelations.newInstance(), AddInitReadHandling.newInstance(), RemoveDeadRelations.newInstance(), MergeEquivalentRelations.newInstance(), diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/ConstraintCopier.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/ConstraintCopier.java index 61bb5902a0..bfc999dbba 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/ConstraintCopier.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/utils/ConstraintCopier.java @@ -121,11 +121,6 @@ public CartesianProduct visitProduct(CartesianProduct def) { return new CartesianProduct(translate(def.getDefinedRelation()), def.getFirstFilter(), def.getSecondFilter()); } - @Override - public Fences visitFences(Fences fence) { - return new Fences(translate(fence.getDefinedRelation()), fence.getFilter()); - } - @Override public Definition.Undefined visitUndefined(Definition.Undefined def) { return new Definition.Undefined(translate(def.getDefinedRelation()));