DijkstraPreventsDeadlocks shows a bug in the translation

[jonnybest]

"Bug in the translation of a modified DijkstraPreventsDeadlocks assertion. It retruns unsat but should returns sat."

Source file:

module examples/algorithms/dijkstra

/*
 * Models how mutexes are grabbed and released by processes, and
 * how Dijkstra's mutex ordering criterion can prevent deadlocks.
 *
 * For a detailed description, see:
 *   E. W. Dijkstra, Cooperating sequential processes. Technological
 *   University, Eindhoven, The Netherlands, September 1965.
 *   Reprinted in Programming Languages, F. Genuys, Ed., Academic
 *   Press, New York, 1968, 43-112.
 */

open util/ordering [State] as so
open util/ordering [Mutex] as mo

sig Process {}
sig Mutex {}

sig State { holds, waits: Process -> Mutex }

pred Initial [s: State]  { no s.holds + s.waits }

pred IsFree [s: State, m: Mutex] {
   // no process holds this mutex
   no m.~(s.holds)
   // all p: Process | m !in p.(this.holds)
}

pred IsStalled [s: State, p: Process] { some p.(s.waits) }

pred GrabMutex [s: State, p: Process, m: Mutex, s': State] {
   // a process can only act if it is not
   // waiting for a mutex
   !s.IsStalled[p]
   // can only grab a mutex we do not yet hold
   m !in p.(s.holds)
   s.IsFree[m] => {
      // if the mutex is free, we now hold it,
      // and do not become stalled
      p.(s'.holds) = p.(s.holds) + m
      no p.(s'.waits)
   } else {
    // if the mutex was not free,
    // we still hold the same mutexes we held,
    // and are now waiting on the mutex
    // that we tried to grab.
    p.(s'.holds) = p.(s.holds)
    p.(s'.waits) = m
  }
  all otherProc: Process - p | {
     otherProc.(s'.holds) = otherProc.(s.holds)
     otherProc.(s'.waits) = otherProc.(s.waits)
  }
}

pred ReleaseMutex [s: State, p: Process, m: Mutex, s': State] {
   !s.IsStalled[p]
   m in p.(s.holds)
   p.(s'.holds) = p.(s.holds) - m
   no p.(s'.waits)
   no m.~(s.waits) => {
      no m.~(s'.holds)
      no m.~(s'.waits)
   } else {
      some lucky: m.~(s.waits) | {
        m.~(s'.waits) = m.~(s.waits) - lucky
        m.~(s'.holds) = lucky
      }
   }
  all mu: Mutex - m {
    mu.~(s'.waits) = mu.~(s.waits)
    mu.~(s'.holds)= mu.~(s.holds)
  }
}

// for every adjacent (pre,post) pair of States,
// one action happens: either some process grabs a mutex,
// or some process releases a mutex,
// or nothing happens (have to allow this to show deadlocks)
pred GrabOrRelease  {
    Initial[so/first] &&
    (
    all pre: State - so/last  | let post = so/next [pre] |
       (post.holds = pre.holds && post.waits = pre.waits)
        ||
       (some p: Process, m: Mutex | pre.GrabMutex [p, m, post])
        ||
       (some p: Process, m: Mutex | pre.ReleaseMutex [p, m, post])

    )
}

pred Deadlock  {
         some Process
         some s: State | all p: Process | some p.(s.waits)
}

pred GrabbedInOrder  {
   all pre: State - so/last |
     let post = so/next[pre] |
        let had = Process.(pre.holds), have = Process.(post.holds) |
        let grabbed = have - had |
           some grabbed => grabbed in mo/nexts[had]
}

assert DijkstraPreventsDeadlocks {
   some Process && //GrabOrRelease && 
   GrabbedInOrder => ! Deadlock
}

pred ShowDijkstra  {
    GrabOrRelease && Deadlock
    some waits
}

//run Deadlock for 3 expect 1
//run ShowDijkstra for 5 State, 2 Process, 2 Mutex expect 1
check DijkstraPreventsDeadlocks for 5 State, 5 Process, 4 Mutex expect 0

[jonnybest]

I found out that the two lemmas about transitive closure are probably wrong. The proof files transcloslemmaproof1.smt2 (see online) and transcloslemmaproof2.smt2 (http://rise4fun.com/Z3/ACHa) show that the two lemmas are not valid.

Here are the two lemmas for reference: 1 (forall ((a1 Atom)(a2 Atom)(r Rel2)) (=> (in_2 a1 a2 (transClos r)) (exists ((a3 Atom)) (and (in_2 a1 a3 r) (in_2 a3 a2 (transClos r)))))) 2 (forall ((a1 Atom)(a2 Atom)(r Rel2)) (=> (in_2 a1 a2 (transClos r)) (exists ((a3 Atom)) (and (in_2 a1 a3 (transClos r)) (in_2 a3 a2 r)))))

Since they are in the core and deleting them from the VC makes the problem 'unknonw', I suspect that they are resposible for this issue #27.

[jonnybest]

Looking at the WP page for the closure operator, I don't think we are doing the right thing here. Judging from the layout, our operator should have four axioms:

1. cl is transitive
2. cl is extensive
3. cl is increasing
4. cl is idempotent

Right now we have the (subset_2 r (transClos r)) which means extensive, and (trans (transClos r)) which means transitive. Our third axiom (=> (and (subset_2 r1 r2) (trans r2)) (subset_2 (transClos r1) r2)) does not actually satisfy minimality. The model we found there was this:

| Rel2_val_0 | Rel2_val_1 | tcl(Rel2_val_0)
|  2 -> 3    |   0 -> 1   |   2 -> 3
|  3 -> 4    |   3 -> 4   |   3 -> 4
             |   2 -> 3   |   2 -> 4
             |   2 -> 4   | 

The problem is that the solver actually set transClos( x ) = Rel2_val_1. That is obviously wrong since Rel2_val_1 is not minimal. Right now I don't know whether that helps me with this particular bug. The one axiom from the core we use is the extensive axiom and that one I believe is correct. So for now we don't know whether the lemma is actually false with respect to a correct set of axioms. I will look for that next.

[jonnybest]

changing to the new 4 axioms fixed the buggy dijkstra. closing this issue.

[jonnybest]

I found the core! It is (ax7 ax8 ax11 ax12 ax13 ax24 ax25 ax26 ax28 ax29 ax34 ax35 ax39 a1 a4 a10 c0 l0) See 4c356f1f6fe0e37627b3acd6c957889153aa5bc9

[jonnybest]

I have gotten a smaller core (ax7 ax8 ax11 ax12 ax13 ax24 ax28 ax29 ax34 ax35 ax39 a1 a4 a10 c0 l0), but was not able to strip the missing assertions in order to test for an even smaller one.

This one may be minimal.

[jonnybest]

The reduced_dijkstra_buggy.als problem contains only the operators which produce the core in core.smt2. Of course, reduced_dijkstra_buggy.smt2 contains more than the minimal axioms. The interesting find is that the only axioms which are in the core and not in the reduced model are transClos axioms and lemmas.

I have looked at the supposedly 'sat' model for dijkstra_buggy.als and compared the resulting statements. The Model from Alloy contains only three Atoms, one in each Mutex, State and Process. These three atoms also make up 'waits'. This results in deadlock=true, so the check is invalid (because of found counter-example). The problem with this model is that it contradicts my closure operator as introduced in 096ee751f58300b536f0398b92a01517480ae64a.

That should not be.

[jonnybest]

Proof of inconsistency:

1 Suppose lemma 1 is correct. forall ((a1 Atom)(a3 Atom)(R Rel2)) (=> (in_2 a1 a3 (transClos R)) (forall ((a2 Atom)) (or (not (in_2 a1 a2 R)) (and (in_2 a1 a2 R) (in_2 a2 a3 (transClos R))))))) 2 Let Mutex = {m0}, Process = {p0}, State = {s0}, waits = {s0->p0->m0}. 3 Let J = join1x1(State, Process) = {s0 -> p0}. 4 tcl(tcl(J)) tcl(J) = J = {s0 -> p0}

Instanziiere nun das Lemma: 5 Let a1 = s0, a2 = a3 = p0. 6 Dann ist in_2 a1 a2 R und es muss gelten: (in_2 a2 a3 (transClos R)) = (in_2 p0 p0 (transClos R)) 7 Das steht im Widerspruch zur 4. Damit ist das Lemma inkonsistent.

Irritierenderweise ist dieses "Lemma 1" mit den in 096ee751f58300b536f0398b92a01517480ae64a eingeführten Axiomen konsistent. Die Axiome sind also wahrscheinlich ebenfalls falsch.