On Proving Confluence of Concurrent Programsby All-Path Reachability of LCTRSs
Misaki Kojima

Naoki Nishida

Nagoya University
IWC 2024, 9th July, 2024

Contents of This Talk
1. Background
2. All-path Reachability Problems of LCTRSs
3. Confluence w.r.t. Initial Terms
4. Conclusion

Background
Concurrent program/ transformation/ concurrent LCTRS/ APR analysis/ result• LCTRSs model concurrent programs▶

All-path reachability (APR) analysis for runtime-error verification• Most concurrent LCTRSs are▶
▶

non-terminatingoverlapping (with non-trivial CPs)

• Some LCTRSs are confluent w.r.t. an initial ground term▶

Despite not satisfy the well-known criteria for confluence• Well-known criteria for confluence are▶
▶

termination + joinability of CPs(weak) orthogonality = left-linear + non-overlapping (triviality of CPs)

2/15

Purpose and Results
PurposeDevelop a method to prove confluence w.r.t. initial term s0 of concurrent LCTRSs
s0∗

t1

∗

~

∗·~

∗t2

ResultShow how to prove joinability of two reachable terms of s0 by APR proofs

Approach• A sufficient condition is that all reachable terms can be reduced back to s0• Solve APR problem {reachable terms} ⇒ {s0 }3/15Contents of This Talk
1. Background
2. All-path Reachability Problems of LCTRSs
3. Confluence w.r.t. Initial Terms
4. Conclusion

Logically Constrained Term Rewrite System (LCTRS)[Kop and Nishida, 2013]• Computation models for functional and imperative languages• Represent asynchronous integer transitions systems

Examplefact(x) → subfact(x, 1)
[x ≤ 0]R2 = subfact(x, y ) → ysubfact(x, y ) → subfact(x − 1, x × y ) [ x > 0 ]

fact(3) →R2 subfact(3, 1)→R2 subfact(3 − 1, 3 × 1) →2R2 subfact(2, 3)→R2 subfact(2 − 1, 2 × 3) →2R2 subfact(1, 6)→R2 subfact(1 − 1, 1 × 6) →2R2 subfact(0, 6)
→R2 6

4/15

LCTRSs for Asynchronous ITSs [Kojima and Nishida, 2023]
Example (Peterson’s mutual exclusion [Baier and Katoen, 2008])
Process 1:

/ noncrit1 l ⟨b1 ,x⟩:=⟨true,2⟩ / wait1Process 2:

/ noncrit2 l ⟨b2 ,x⟩:=⟨true,1⟩ / wait2x=1 ∨ ¬b2/ crit1

x=2 ∨ ¬b1/ crit2b1 :=false

b2 :=false• bi indicates that Process i wants to enter the critical section• x indicates that Process x has priority for the critical section• Asynchronous ITS for Processes 1 & 2 is represented bycnfg(noncrit1 , p2 ,cnfg(wait1 , p2 ,cnfg(crit1 ,p2 ,
cnfg(p1 ,cnfg(p1 ,cnfg(p1 ,b1′ , b2 , x ′ )b1 , b2 , x )b1′ , b2 , x )[ b1′ = true ∧ x ′ = 2 ]
[ x = 1 ∨ ¬b2 ]′[ b1 = false ]wait2 , b1 , b2′ , x ′ )crit2 ,b1 , b2 , x )noncrit2 , b1 , b2′ , x )[ b2′ = true ∧ x ′ = 1 ]
[ x = 2 ∨ ¬b1 ]′[ b1 = false ]b1 , b2 , x) → cnfg(wait1 , p2 ,b1 , b2 , x) → cnfg(crit1 ,p2 ,b1 , b2 , x) → cnfg(noncrit1 , p2 ,noncrit2 , b1 , b2 , x) → cnfg(p1 ,wait2 , b1 , b2 , x) → cnfg(p1 ,crit2 ,b1 , b2 , x) → cnfg(p1 ,5/15

All-Path Reachability Problems of LCTRSs[Ciobâcă and Lucanu, 2018]• Constrained term ⟨t | ϕ⟩▶
▶

t is a term and ϕ is a constraint⟨t | ϕ⟩ represents the set of ground instance tθ such that θ satisfies ϕExampleConstrained term representing the initial state of the previous example⟨cnfg(noncrit1 , noncrit2 , false, false, x) | x = 1 ∨ x = 2⟩

• APR Problem ⟨s | ϕ⟩ ⇒ ⟨t | ψ⟩• Execution path = finite and ends with an irreducible state or infinite

Demonical validity of ⟨s | ϕ⟩ ⇒ ⟨t | ψ⟩Every finite execution path from a state in ⟨s | ϕ⟩ includes a state in ⟨t | ψ⟩
• Constant-directed APR Problem ⟨s | ϕ⟩ ⇒ ⟨c | true⟩ where c is a constant nf▶

Abbreviate to ⟨s | ϕ⟩ ⇒ c• Proof systems for constant-directed APR problems have been proposed[Kojima and Nishida, 2023]

6/15

Contents of This Talk
1. Background
2. All-path Reachability Problems of LCTRSs
3. Confluence w.r.t. Initial Terms
4. Conclusion

How to Prove Confluence w.r.t. Initial Terms• Prove that all reachable terms of s0 can be reduced back to s0sG 0W

∗

t1~

∗ ∗

∗

t2

• This may be reduced to APR problem {reachable terms} ⇒ {s0 }Difficulties• {reachable terms} cannot be represented by a single constrained term
• Infinite reductions from t1 and t2 are not considered for APR-validity

Approach to difficulties• Take ⟨s0 | true⟩ for {reachable terms}▶
▶

s0 itself is a reachable term
APR problem ⟨s0 | true⟩ ⇒ ⟨s0 | true⟩ is meaningless• Solve APR problem ⟨s0 | true⟩ ⇒ init of R ∪ {s0 → init}▶

init is a fresh constant• Strong connectedness of APR proofs under certain conditions

7/15

c-DCC: Proof System for APR Problems[Kojima and Nishida, 2023]• c-DCC(R, G) : Proof system based on R and the set of APR problems Gaxiom/c-subs⟨s | ϕ⟩ ⇒ cif ϕ is unsatisfiable or s = cc-der⟨s1 | ϕ1 ⟩ ⇒ c . . . ⟨sn | ϕn ⟩ ⇒ cif ⟨s | ϕ⟩ ∩ NF R = ∅⟨s | ϕ⟩ ⇒ cwhere ⟨si | ϕi ⟩ are constrained terms that are reachable in one step from ⟨s | ϕ⟩weak circ⟨s | ϕ⟩ ⇒ cif ∃(⟨s ′ | ϕ′ ⟩ ⇒ c) ∈ G. ⟨s | ϕ⟩ = ⟨s ′ | ϕ′ ⟩8/15

Example (Peterson’s mutual exclusion [Baier and Katoen, 2008])
cnfg(noncrit1 , p2 ,b1 , b2 , x)
→ cnfg(wait1 , p2 ,b1′ , b2 , x ′ )
cnfg(wait1 , p2 ,b1 , b2 , x)
→ cnfg(crit1 ,p2 ,b1 , b2 , x )cnfg(crit1 ,p2 ,b1 , b2 , x)
→ cnfg(noncrit1 , p2 ,b1′ , b2 , x )
cnfg(p1 , noncrit2 ,b1 , b2 , x)
→ cnfg(p1 ,wait2 , b1 , b2′ , x ′ )
cnfg(p,wait,b,b,x)→cnfg(p,crit2 ,b1 , b2 , x )

12
121



cnfg(p1 , crit2 ,b1 , b2 , x)
→ cnfg(p1 ,noncrit2 , b1 , b2′ , x )
cnfg(noncrit1 , noncrit2 , false, false, x) → init
(2)
(3)
(3)
(9) cnfg(n1 , n2 , f, f, 2)(10) cnfg(c1 , w2 , t, t, 1)(10)(5) cnfg(c1 , n2 , t, f, 2)(6) cnfg(w1 , w2 , t, t, 1)(2) cnfg(w1 , n2 , t, f, 2)[ b1′ = true ∧ x ′ = 2 ]
[ x = 1 ∨ ¬b2 ]
[ b1′ = false ]′′[ b2 = true ∧ x = 1 ][ x = 2 ∨ ¬b1 ][ b1′ = false ]



(2)
(11) cnfg(w1 , c2 , t, t, 2)(11)(1)(7) cnfg(w1 , w2 , t, t, 2)(8) cnfg(n1 , c2 , f, t, 1)(3) cnfg(n1 , w2 , f, t, 1)(1) cnfg(n1 , n2 , f, f, 1)(4) init• Note that ⟨s | true⟩ ⇒ init abbreviated to s in the above tree
• APR problem ⟨s0 | true⟩ ⇒ init of R ∪ {s0 → init} is solved• All terms are reduced to (1)?
▶
▶

Yes, and thus confluent(4) don’t have to be considered• Does validity of APR problem imply joinability of all reachable terms?
▶

No9/15

Necessity of Strong Connectedness
Example

a→b 


 a→c 

b→b
R=

c→c 

a → init(2)(2) ⟨b | true⟩ ⇒ init(3)(3) ⟨c | true⟩ ⇒ init
(1) ⟨a | true⟩ ⇒ init(4) ⟨init | true⟩ ⇒ init

• ⟨a | true⟩ ⇒ init is valid but R is not confluent• Any infinite path not reaching initial term is not considered for APR-validity• To consider them, we need strong connectedness▶

Ignore (4) ⟨init | true⟩ ⇒ init

10/15

Examplep2 , b1′ , b2 , x ′ )p2 , b1 , b2 , x )p2 , b1 , b2 , x) → cnfg(noncrit1 , p2 , b1′ , b2 , x )..
.

[ b1′ = true ∧ x ′ = 2 ]
[ x = 1 ∨ ¬b2 ]′[ b1 = false ]





cnfg(noncrit1 , p2 , b1 , b2 , x) → cnfg(wait1 ,cnfg(wait1 , p2 , b1 , b2 , x) → cnfg(crit1 ,cnfg(crit1 ,



(9) d

9(5) e

(10)

O(11)

(6)

(7)

OO. (2)

% ye
9 (8)

O

9 (3)
e(1) pExamplea→b 
 a→c 

b→b
R=


 c→c 
a → init(2) d: (3)
(1)

11/15

Strong Connectedness is NOT Sufficient• Strong connectedness does not imply joinability of all reachable terms

Examplef(x) → g(x, y ) [ y ≥ x ]R2 = g(x, y ) → f(x) [ y ≤ x ]
h(x, y ) → f(x) [ y ≤ x ]f(x) → h(x, y ) [ y ≥ x ]g(x, y ) → g(x, y ′ ) [ y > x ∧ y ′ = y + 1 ]h(x, y ) → h(x, y ′ ) [ y > x ∧ y ′ = y + 1 ]⟨g(0, y ) | 0 ≤ y ⟩ ⇒ init⟨h(0, y ) | 0 ≤ y ⟩ ⇒ init⟨f(0) | true⟩ ⇒ init

• The proof tree is strongly connected• But R2 is not confluent w.r.t. f(0)• There exists a cyclic path such that1. ⟨g(x, y ) | x ≤ y ⟩ ⇒ init contains two or more terms, and
2. s0 is not contained

12/15

Our Confluence Criterion• All reachable terms can be reduced to s0 if
1. all constrained terms are singleton sets, or
2. there is no cycle not including s0Theorem (main result)
Let G be a proof tree for APR problem ⟨s0 | true⟩ ⇒ init of R ∪ {s0 → init}.
Suppose that G is strongly connected and one of the following holds:
1. for every node of G , ⟨s | ϕ⟩ of the attached ⟨s | ϕ⟩ ⇒ init is singleton, or
2. G \ {root node} is acyclic.
Then, R is confluent w.r.t. s0 .

13/15

Remarks• We have not adapted our APR prover Crisys2cdcc to our confluence criterion• The example (Peterson’s mutual exclusion) in this talk is linear and all its CPs
are strongly closed and thus strongly confluent [Schöpf and Middeldorp, 2023]
crest1 [Schöpf and Middeldorp, 2024] succeeds in proving its confluence▶ crest failed to prove confluence of the LCTRS obtained from it by adding
some redundant rules (ℓ → ℓ)▶

1 http://cl-informatik.uibk.ac.at/software/crest/14/15

Contents of This Talk
1. Background
2. All-path Reachability Problems of LCTRSs
3. Confluence w.r.t. Initial Terms
4. Conclusion

Conclusion
SummaryShow how to prove joinability of two reachable terms of s0 by APR proofs

Future Work• Implementation• Relax our sufficient condition▶

Each CP can be reduced to its critical peak∗t1

3 t0 k∗∗3 t2 k~
t3~

∗t4

15/15

References
Baier, C. and Katoen, J. (2008).
Principles of model checking.
MIT Press.
Ciobâcă, Ş. and Lucanu, D. (2018).
A coinductive approach to proving reachability properties in logically constrained term rewriting
systems.
In Galmiche, D., Schulz, S., and Sebastiani, R., editors, Proceedings of the 9th International
Joint Conference on Automated Reasoning, volume 10900 of Lecture Notes in Computer
Science, pages 295–311. Springer.
Kojima, M. and Nishida, N. (2023).
Reducing non-occurrence of specified runtime errors to all-path reachability problems ofconstrained rewriting.
Journal of Logical and Algebraic Methods in Programming, 135:1–19.
Kop, C. and Nishida, N. (2013).
Term rewriting with logical constraints.
In Fontaine, P., Ringeissen, C., and Schmidt, R. A., editors, Proceedings of the 9thInternational Symposium on Frontiers of Combining Systems, volume 8152 of Lecture Notes in
Artificial Intelligence, pages 343–358.

References (cont.)
Schöpf, J. and Middeldorp, A. (2023).
Confluence criteria for logically constrained rewrite systems.
In Pientka, B. and Tinelli, C., editors, Proceedings of the 29th International Conference on
Automated Deduction, volume 14132 of Lecture Notes in Computer Science, pages 474–490.
Springer.
Schöpf, J. and Middeldorp, A. (2024).
crest 0.8.
In Chenavier, C. and Nishida, N., editors, Proceedings of the 13th International Workshop onConfluence, pages 66–66.