[RA] Missing tuples in transitive closure

[hernanponcedeleon]

While debugging the differences between the datalog and native backends for the RA in #708 , @DIvanov503 and I found what seems to be a bug in the computation of deltas for the transitive closure of relations.

This propagator is called twice (once by the RA and once by the encode via a call to populateQueue). AFAIK the second call should not add more may pairs (it could however drop some), but it indeed does

[13.08.2024] 11:28:57 [INFO] RelationAnalysis.fromConfig - Selected relation analysis: NATIVE
[13.08.2024] 11:28:57 [INFO] RelationAnalysis.fromConfig - 
        wmm.analysis.relationAnalysis: NATIVE
        wmm.analysis.extendedRelationAnalysis: false
====== // First call
[] := cumul-fence^+
[(5,8)(5,10)(5,11)(5,23)(5,25)(5,27)(6,8)(6,10)(6,11)(6,23)(6,25)(6,27)(10,8)(10,10)(10,11)(10,23)(10,25)(10,27)(11,8)(11,10)(11,11)(11,23)(11,25)(11,27)(14,27)(25,8)(25,10)(25,11)(25,23)(25,25)(25,27)(27,8)(27,10)(27,11)(27,23)(27,25)(27,27)(54,8)(54,10)(54,11)(54,23)(54,25)(54,27)(78,8)(78,10)(78,11)(78,23)(78,25)(78,27)(102,8)(102,10)(102,11)(102,23)(102,25)(102,27)]
======
....
[13.08.2024] 11:28:58 [INFO] Acyclicity.getEncodeGraph - Computing encodeGraph for acyclic cumul-fence^+
[13.08.2024] 11:28:58 [INFO] Acyclicity.getEncodeGraph - encodeGraph size: 16
[13.08.2024] 11:28:58 [INFO] Acyclicity.getEncodeGraph - reduced encodeGraph size: 16
====== // Second call
[] := cumul-fence^+
[(5,8)(5,10)(5,11)(5,23)(5,25)(5,27)(6,8)(6,10)(6,11)(6,23)(6,25)(6,27)(10,8)(10,10)(10,11)(10,23)(10,25)(10,27)(11,8)(11,10)(11,11)(11,23)(11,25)(11,27)(14,23)(14,25)(14,27)(25,8)(25,10)(25,11)(25,23)(25,25)(25,27)(27,8)(27,10)(27,11)(27,23)(27,25)(27,27)(54,8)(54,10)(54,11)(54,23)(54,25)(54,27)(78,8)(78,10)(78,11)(78,23)(78,25)(78,27)(102,8)(102,10)(102,11)(102,23)(102,25)(102,27)]

The second one has pair (14,23) which could be derived from (14,27) and (27,23). The first call has the later two, but missed the former.

Here are a "minimal" model and test case to reproduce

let po-rel = po ; [Release]
let po-unlock-lock-po = (po|rf) ; [LKR]

let cumul-fence = (rfe ; po-rel | po-unlock-lock-po) ; (rmw)*

acyclic cumul-fence+ as happens-before

and

C C-PaulEMcKenney-psc+sr-relonce

(*
 * Result: Sometimes
 *)

{}

P0(int *x, int *y, int *be_careful, spinlock_t *cl)
{
    int r1;
    int r2;

    rcu_read_lock();
    r1 = READ_ONCE(*be_careful);
    if (r1) {
        spin_lock(cl);
        spin_unlock(cl);
    } else {
        WRITE_ONCE(*y, 1);
    }
    rcu_read_unlock();
}

P1(int *x, int *y, int *be_careful, spinlock_t *cl)
{
    int r1;

    spin_lock(cl);
    r1 = READ_ONCE(*y);
    spin_unlock(cl);
}

locations [0:r1]
exists (0:r2=1 \/ 1:r1=1)

[ThomasHaas]

Can you map back the event ids to the lines of code (I know that we do not have source information for Litmus code)?

[hernanponcedeleon]

23: read part of spinlock in P1 27: READ_ONCE in P1 14: WRITE_ONCE in P0

[ThomasHaas]

The example shows what I mentioned in #718 (and what I meant when saying "check the litmus tests manually"). Our analysis is likely correct and the "missing tuples" are not really missing, they are unnecessary. The edge (27, 23) is formed by a chain that goes through the first branch of P0 and is thus mutually exclusive to the 14: WRITE_ONCE event. By performing suboptimal TC computation, in particular, by performing the computation twice, you end up with this imprecision. This is because our current implementation is somewhat awkwardly implemented: it performs update operations that are a hybrid between a linear TC formulation (r+;r) and the quadratic formulation (r+;r+). This causes it to degenerate to the quadratic solution when repeated unnecessarily often. This quadratic solution is the least precise one and is also the one computed in the Datalog version.