The system models a concurrent Garbage Collector. Memory locations are modelled as nodes with two pointers. The user program is modelled by the mutator, which can change pointers to point to some accessible node in the graph. The collector carries out the garbage collection and it runs concurrently. Full correctness of the garbage collector means that the following two properties should hold:
With our tool, we have been able to prove the first property. The second property is a liveness condition and our methods are only applicable to safety properties.
(murphi-program ;; Constant decls... (constant-decls (WHITE 0) (GRAY 1) (BLACK 2) (MUTATE 0) (COLORING 1) (COLOR-ROOTS 2) (MARKING-PHASE 3) (TEST-K 4) (COLOR-CHILD 5) (INCREMENT-I 6) (APPENDING-PHASE 7) (TEST-J 8) (APPEND 9) (INCREMENT 10)) ;; State decls... (input (nn rat) (pp rat) (kk rat)) (global-state (color (array rat)) (son (array rat)) (son-orig (array rat)) (mutator-loc rat) (collector-loc rat) (q rat) (r rat) (l rat) (NODES rat) ;(i rat) (j rat) (k rat) (c rat) (error bool)) ;; Axioms... (axiom (and (> NODES 0) (forall (p) (and (< (aref son-orig p) NODES) (>= (aref son-orig p) 0))) (forall (p) (forall (q) (<=> (> p q) (>= p (+ q 1))))))) (function accessible (bool ((array rat) rat)) (and (accessible son 0) (accessible son-orig 0) (forall (p) (=> (accessible son p) (accessible son (aref son p)))) (=> (and (/= (aref color 0) WHITE) (forall (x) (=> (and (>= x 0) (< x NODES) (/= (aref color x) WHITE)) (/= (aref color (aref son x)) WHITE)))) (=> (accessible son kk) (/= (aref color kk) WHITE))) (=> (and (= (aref color 0) BLACK) (forall (p) (=> (and (= (aref color p) BLACK) (>= p 0) (< p NODES)) (= (aref color (aref son p)) BLACK)))) (forall (q) (=> (accessible son q) (= (aref color q) BLACK)))) (forall (x) (=> (and (accessible son kk) (accessible (write son nn kk) x)) (accessible son x))) (=> (accessible son kk) (accessible (write son nn kk) kk)))) ;; Initialization rule... (initialize (progn (setq j 0) (setq k 0) (setq q 0) (setq son son-orig) (setq (aref color 0) WHITE) (setq color (mwrite color p true WHITE)) (setq collector-loc COLOR-ROOTS) (setq mutator-loc MUTATE) (setq error false))) ;; Mutator rules... (rules (==> (and (= mutator-loc MUTATE) (or true (= collector-loc COLOR-ROOTS))) (ite (and (accessible son kk) (>= kk 0) (< kk NODES)) (progn (setq (aref son nn) kk) (ite (= (aref color kk) WHITE) (setq (aref color kk) GRAY) (skip))) (skip)))) ;; Collector Rules... (rules (==> "Collector0" (= collector-loc COLOR-ROOTS) (progn (setq j 0) (setq k 0) (setq (aref color 0) GRAY) (setq collector-loc MARKING-PHASE))) (==> (= collector-loc MARKING-PHASE) (progn (setq collector-loc TEST-K))) (==> (and (= collector-loc TEST-K) (>= k NODES)) (setq collector-loc APPENDING-PHASE)) (==> (and (= collector-loc TEST-K) (not (>= k NODES))) (setq collector-loc COLOR-CHILD)) (==> "Collector1" (and (= collector-loc COLOR-CHILD) (= (aref color k) GRAY) (or true (= (aref color NODES) BLACK))) (progn (ite (= (aref color (aref son k)) WHITE) (setq (aref color (aref son k)) GRAY) (skip)) (setq (aref color k) BLACK) (setq k 0) (setq collector-loc TEST-K))) (==> (and (= collector-loc COLOR-CHILD) (not (= (aref color k) GRAY)) (or true (= (aref color (- k 1)) BLACK))) (progn (setq k (+ k 1)) (setq collector-loc TEST-K))) (==> (= collector-loc APPENDING-PHASE) (progn (setq j 0) (setq collector-loc TEST-J))) (==> (and (= collector-loc TEST-J) (= (aref color j) WHITE) (not (>= j NODES))) (setq collector-loc APPEND)) (==> (and (= collector-loc TEST-J) (not (= (aref color j) WHITE)) (not (>= j NODES))) (progn (setq (aref color j) WHITE) (setq j (+ j 1)))) (==> (and (= collector-loc TEST-J) (>= j NODES)) (progn (setq j 0) (setq collector-loc COLOR-ROOTS))) (==> (= collector-loc APPEND) (progn ;; Test if we are freeing something wrong... (ite (accessible son j) (setq error true) (skip)) (setq j (+ j 1)) (setq collector-loc TEST-J)))) ;; Invariant... (invariant (not error)) (candidate-invariants D421 D11 D12 D13 D14 D15 D16 D17 D18 D21 D22 D32) (pseudo-invariants D34) ;; Abstract state... (abstraction (B0 error B0 D15 D16 D17 J=0 J>0 J>=NODES COLOR[J]=WHITE) (M@MUTATE (= mutator-loc MUTATE)) (M@COLORING (= mutator-loc COLORING)) (C@COLOR-ROOTS (= collector-loc COLOR-ROOTS)) (C@MARKING-PHASE (= collector-loc MARKING-PHASE)) (C@TEST-K (= collector-loc TEST-K)) (C@COLOR-CHILD (= collector-loc COLOR-CHILD)) (C@APPENDING-PHASE (= collector-loc APPENDING-PHASE)) (C@TEST-J (= collector-loc TEST-J)) (C@APPEND (= collector-loc APPEND)) (D421 (and (>= q 0) (< q NODES))) ;(D422 (=> (= mutator-loc COLORING) (accessible son q))) (D11 (forall (x) (and (>= (aref son x) 0) (< (aref son x) NODES)))) (D12 (forall (x) (or (= (aref color x) WHITE) (= (aref color x) BLACK) (= (aref color x) GRAY)))) (D13 (forall (x) (=> (= collector-loc COLOR-ROOTS) (=> (and (>= x 0) (< x NODES)) (/= (aref color x) BLACK))))) (D14 (forall (x) (=> (= collector-loc APPENDING-PHASE) (and (=> (and (>= x 0) (< x NODES) (accessible son x)) (= (aref color x) BLACK)) (=> (and (>= x 0) (< x NODES)) (and (/= (aref color x) GRAY) (=> (= (aref color x) BLACK) (= (aref color (aref son x)) BLACK)))) (= (aref color 0) BLACK))))) (D15 (forall (x) (=> (= collector-loc TEST-J) (and (=> (and (>= x j) (< x NODES) (accessible son x)) (= (aref color x) BLACK)) (=> (and (< x j) (>= x 0)) (/= (aref color x) BLACK)) (=> (and (>= x j) (< x NODES)) (/= (aref color x) GRAY)))))) (D16 (forall (x) (=> (= collector-loc APPEND) (and (=> (and (>= x j) (< x NODES) (accessible son x)) (= (aref color x) BLACK)) (=> (and (< x j) (>= x 0)) (/= (aref color x) BLACK)) (=> (and (>= x j) (< x NODES)) (/= (aref color x) GRAY)) (not (accessible son j)) (= (aref color j) WHITE))))) (D17 (=> (or (= collector-loc COLOR-ROOTS) (= collector-loc MARKING-PHASE) (= collector-loc APPENDING-PHASE) (= collector-loc TEST-K) (= collector-loc COLOR-CHILD)) (and (= j 0) (or true (= (aref color j) WHITE))))) (D18 (forall (x) (=> (or (= collector-loc TEST-K) (= collector-loc COLOR-CHILD)) (=> (and (>= x 0) (< x k) (accessible son x)) (= (aref color x) BLACK))))) (D21 (=> (and (or (= collector-loc MARKING-PHASE) (= collector-loc TEST-K) (= collector-loc COLOR-CHILD)) (= mutator-loc MUTATE)) (forall (x) (=> (and (>= x 0) (< x NODES) (= (aref color x) BLACK)) (/= (aref color (aref son x)) WHITE))))) (D22 (=> (and (or (= collector-loc MARKING-PHASE) (= collector-loc TEST-K) (= collector-loc COLOR-CHILD)) (= mutator-loc COLORING)) (forall (x) (=> (and (>= x 0) (< x NODES) (/= x r) (= (aref color x) BLACK)) (/= (aref color (aref son x)) WHITE))))) (j=0 (= j 0)) (j>0 (> j 0)) (j>=NODES (>= j NODES)) (k=0 (= k 0)) (k>0 (> k 0)) (k>=NODES (>= k NODES)) (color[0]=GRAY (= (aref color 0) GRAY)) (color[0]=BLACK (= (aref color 0) BLACK)) (color[0]=WHITE (= (aref color 0) WHITE)) (color[k]=GRAY (= (aref color k) GRAY)) (color[j]=WHITE (= (aref color j) WHITE)) (D31 (forall (x) (=> (and (>= x 0) (< x k) (or true (= (aref color kk) WHITE)) (or true (= (aref color pp) WHITE))) (/= (aref color x) GRAY)))) (D32 (forall (x) (=> (and (>= x 0) (< x NODES) (or true (= k 0))) (=> (= (aref color x) BLACK) (or (= (aref color (aref son x)) GRAY) (= (aref color (aref son x)) BLACK)))))) ))