[demarkok]

When the .cat memory model compiles into an SMT problem, acyclic r turns into the axiomatic definition of r⁺ (i.e. r ⊆ r⁺ and r⁺ ; r⁺ ⊆ r⁺) and the irreflexivity check for r⁺. I think z3 doesn't solve it very efficiently. In particular, when the 3 quantifiers of r⁺ ; r⁺ ⊆ r⁺ (i.e. ∀a,b,c. r⁺ a b -> r⁺ b c -> r⁺ a c) are eliminated, N^3 instances are generated.

Instead, one can define a function clock : Event -> Int with the axiom r e1 e2 ⇒ clock(e1) < clock(e2). It exists if and only if r is acyclic. There are only two quantifiers to eliminate, so N^2 instances are generated, and after that, I think z3 might deal better with integers.

I ran some tests through the web interface, online and locally. The tests (see below, in the "details") are MP through N locations. Even for N = 8, the upstream web interface takes a minute to finish.

In aarch64.cat, I also changed irreflexive ob as external to acyclic obs | dob | aob | bob as external, as now acyclic doesn't require calculating the full transitive closure. Even on its own, this change in .cat file speeds up the tests quite a bit, but N = 24 still times out.

With the clock encoding, it finishes in seconds.

Perhaps we could run proper benchmarks, but this encoding seems semantically sound and does improve performance. I used Claude to run some benchmarks through the command line, on MPn-N (MP with N data locations, 2N+3 events): one worker thread, --check-sat-using "(par-or smt (then dt2bv simplify solve-eqs qe bv))", z3 capped at 120 s. z3 time per test:

test	upstream	cat change only	this PR
MPn-4	0.7 s	0.7 s	0.6 s
MPn-8	2.0 s	2.5 s	0.9 s
MPn-16	> 120 s	7.6 s	1.7 s
MPn-24	> 120 s	> 120 s	3.1 s

"Cat change only" is the upstream binary with just the aarch64.cat edit. The 48 tests in web/client/dist/aarch64 give the same verdicts as before and take about the same time.

Details

N = 4

arch = "AArch64"
name = "MPn-4"
symbolic = ["x1", "x2", "x3", "x4", "y"]

[thread.0]
init = { X1 = "x1", X2 = "x2", X3 = "x3", X4 = "x4", X5 = "y" }
code = """
	MOV W0,#1
	STR W0,[X1]
	STR W0,[X2]
	STR W0,[X3]
	STR W0,[X4]
	STR W0,[X5]
"""

[thread.1]
init = { X1 = "x1", X2 = "x2", X3 = "x3", X4 = "x4", X5 = "y" }
code = """
	LDR W5,[X5]
	LDR W1,[X1]
	LDR W2,[X2]
	LDR W3,[X3]
	LDR W4,[X4]
"""

[final]
expect = "sat"
assertion = "1:X5 = 1 & 1:X1 = 0 & 1:X2 = 0 & 1:X3 = 0 & 1:X4 = 0"

N = 24

arch = "AArch64"
name = "MPn-24"
symbolic = ["x1", "x2", "x3", "x4", "x5", "x6", "x7", "x8", "x9", "x10", "x11", "x12", "x13", "x14", "x15", "x16", "x17", "x18", "x19", "x20", "x21", "x22", "x23", "x24", "y"]

[thread.0]
init = { X1 = "x1", X2 = "x2", X3 = "x3", X4 = "x4", X5 = "x5", X6 = "x6", X7 = "x7", X8 = "x8", X9 = "x9", X10 = "x10", X11 = "x11", X12 = "x12", X13 = "x13", X14 = "x14", X15 = "x15", X16 = "x16", X17 = "x17", X18 = "x18", X19 = "x19", X20 = "x20", X21 = "x21", X22 = "x22", X23 = "x23", X24 = "x24", X25 = "y" }
code = """
	MOV W0,#1
	STR W0,[X1]
	STR W0,[X2]
	STR W0,[X3]
	STR W0,[X4]
	STR W0,[X5]
	STR W0,[X6]
	STR W0,[X7]
	STR W0,[X8]
	STR W0,[X9]
	STR W0,[X10]
	STR W0,[X11]
	STR W0,[X12]
	STR W0,[X13]
	STR W0,[X14]
	STR W0,[X15]
	STR W0,[X16]
	STR W0,[X17]
	STR W0,[X18]
	STR W0,[X19]
	STR W0,[X20]
	STR W0,[X21]
	STR W0,[X22]
	STR W0,[X23]
	STR W0,[X24]
	STR W0,[X25]
"""

[thread.1]
init = { X1 = "x1", X2 = "x2", X3 = "x3", X4 = "x4", X5 = "x5", X6 = "x6", X7 = "x7", X8 = "x8", X9 = "x9", X10 = "x10", X11 = "x11", X12 = "x12", X13 = "x13", X14 = "x14", X15 = "x15", X16 = "x16", X17 = "x17", X18 = "x18", X19 = "x19", X20 = "x20", X21 = "x21", X22 = "x22", X23 = "x23", X24 = "x24", X25 = "y" }
code = """
	LDR W25,[X25]
	LDR W1,[X1]
	LDR W2,[X2]
	LDR W3,[X3]
	LDR W4,[X4]
	LDR W5,[X5]
	LDR W6,[X6]
	LDR W7,[X7]
	LDR W8,[X8]
	LDR W9,[X9]
	LDR W10,[X10]
	LDR W11,[X11]
	LDR W12,[X12]
	LDR W13,[X13]
	LDR W14,[X14]
	LDR W15,[X15]
	LDR W16,[X16]
	LDR W17,[X17]
	LDR W18,[X18]
	LDR W19,[X19]
	LDR W20,[X20]
	LDR W21,[X21]
	LDR W22,[X22]
	LDR W23,[X23]
	LDR W24,[X24]
"""

[final]
expect = "sat"
assertion = "1:X25 = 1 & 1:X1 = 0 & 1:X2 = 0 & 1:X3 = 0 & 1:X4 = 0 & 1:X5 = 0 & 1:X6 = 0 & 1:X7 = 0 & 1:X8 = 0 & 1:X9 = 0 & 1:X10 = 0 & 1:X11 = 0 & 1:X12 = 0 & 1:X13 = 0 & 1:X14 = 0 & 1:X15 = 0 & 1:X16 = 0 & 1:X17 = 0 & 1:X18 = 0 & 1:X19 = 0 & 1:X20 = 0 & 1:X21 = 0 & 1:X22 = 0 & 1:X23 = 0 & 1:X24 = 0"

[Alasdair]

Looks great. I wonder if there would be any advantage to using a bitvector clock function with bvult/bvslt, since the number of events is finite? It would keep the entire problem in the bitvector theory, but maybe that doesn't matter much here.

[demarkok]

I tried it with bitvectors, it's slower.
It seems like an integer clock encoding is somehow more natural for z3 than bitvectors in this case. I think it's able to figure out, when working in linear integer arithmetic, that it's actually looking for cycles.

[Alasdair]

Slower than integer clocks, or slower than the naive encoding of transitive closure?

[demarkok]

Slower than integer clocks, or slower than the naive encoding of transitive closure?

Both. I tried __clock : Event -> (_ BitVec 16) with bvult for < on the same tests:

test	closure	Int clocks	bv clocks
MPn-4	1.0 s	0.2 s	1.1 s
MPn-8	2.4 s	0.4 s	4.3 s
MPn-16	>120 s	1.1 s	64.7 s
MPn-24	>120 s	2.4 s	>120 s

My interpretation is that with the bitvector clock, after bit-blasting, SAT has to re-discover transitivity, while for the integer arithmetic solver it's native.

NB: without rewriting irreflexive R⁺ -> acyclic R in the .cat files, the int clocks are sometimes slower than the naive encoding; I think it's a penalty for mixing z3 theories.