Liveness and temporal prophecy

examples/liveness/ticket.ivy

@@ -0,0 +1,275 @@
+#lang ivy1.6
+
+################################################################################
+# A liveness proof of the ticket protocol
+################################################################################
+
+
+################################################################################
+# Module for axiomatizing a total order
+#
+################################################################################
+
+module total_order(r) = {
+    axiom r(X,X)                        # Reflexivity
+    axiom r(X, Y) & r(Y, Z) -> r(X, Z)  # Transitivity
+    axiom r(X, Y) & r(Y, X) -> X = Y    # Anti-symmetry
+    axiom r(X, Y) | r(Y, X)             # Totality
+}
+
+################################################################################
+#
+# Types, relations and functions describing the state
+#
+################################################################################
+
+object ticket_protocol = {
+
+    ################################################################################
+    #
+    # The protocol description
+    #
+    ################################################################################
+
+    type thread
+    type ticket
+
+    relation le(X:ticket, Y:ticket)
+    instantiate total_order(le)
+    individual zero:ticket
+    axiom forall X. le(zero, X)
+
+    relation pc1(T:thread)
+    relation pc2(T:thread)
+    relation pc3(T:thread)
+
+    individual service:ticket
+    individual next_ticket:ticket
+    relation m(T:thread, K:ticket)  # use relation and not a function to be in EPR
+
+    relation scheduled(T:thread)
+
+    init pc1(T)
+    init ~pc2(T)
+    init ~pc3(T)
+    init service = zero
+    init next_ticket = zero
+    init m(T,K) <-> K = zero
+    init ~scheduled(T)
+
+    ################################################################################
+    #
+    # Protocol actions
+    #
+    ################################################################################
+
+    action succ(x:ticket) returns (y:ticket) = {
+        assume ~le(y,x) & forall Z:ticket. ~le(Z,x) -> le(y,Z)
+    }
+
+    action step12(t:thread) = {
+        assume pc1(t);
+        m(t,K) := K = next_ticket;
+        next_ticket := succ(next_ticket);
+        pc1(t) := false;
+        pc2(t) := true;
+        scheduled(T) := T = t;
+    }
+
+    action step22(t:thread, k1:ticket) = {
+        assume pc2(t);
+        assume m(t,k1);
+        assume ~le(k1,service);
+        # stay in pc2
+        scheduled(T) := T = t;
+    }
+
+    action step23(t:thread, k1:ticket) = {
+        assume pc2(t);
+        assume m(t,k1);
+        assume le(k1,service);
+        pc2(t) := false;
+        pc3(t) := true;
+        scheduled(T) := T = t;
+    }
+
+    action step31(t:thread) = {
+        assume pc3(t);
+        service := succ(service);
+        pc3(t) := false;
+        pc1(t) := true;
+        scheduled(T) := T = t;
+    }
+
+    export step12
+    export step22
+    export step23
+    export step31
+
+    ################################################################################
+    #
+    # Conjectures for proving safety (also helps for liveness)
+    #
+    ################################################################################
+
+    # safety property
+    conjecture [safety] pc3(T1) & pc3(T2) -> T1 = T2
+    # basic
+    conjecture pc1(T) | pc2(T) | pc3(T)
+    conjecture ~pc1(T) | ~pc2(T)
+    conjecture ~pc1(T) | ~pc3(T)
+    conjecture ~pc2(T) | ~pc3(T)
+    conjecture m(T,K1) & m(T,K2) -> K1 = K2
+    # inductive invariant for proving safety
+    conjecture next_ticket = zero -> m(T,zero)
+    conjecture next_ticket ~= zero & m(T,M) -> ~le(next_ticket,M)
+    conjecture (pc2(T) | pc3(T)) -> next_ticket ~= zero
+    conjecture m(T1,M) & m(T2,M) & M ~= zero -> T1 = T2
+    conjecture pc2(T) & m(T,M) -> le(service,M)
+    conjecture pc3(T) -> m(T,service)
+    conjecture le(service,next_ticket)
+    conjecture ~(~pc1(T1) & ~pc1(T2) & m(T1,zero) & m(T2,zero) & T1 ~= T2)
+
+
+    ################################################################################
+    #
+    # Temporal property and its proof
+    #
+    ################################################################################
+
+    isolate tp1 = {
+
+        individual sk0:thread  # witness for the formula (exists T0. ~(globally ~(pc2(T0) & globally ~pc3(T0))))
+
+	object spec = {
+            temporal property [nonstarvation] (
+                ((exists T0. ~(globally ~(pc2(T0) & globally ~pc3(T0)))) -> ~(globally ~(pc2(sk0) & globally ~pc3(sk0)))) &
+                (forall T1. globally (eventually scheduled(T1)))
+            ) -> (forall T2. globally ~(pc2(T2) & globally ~pc3(T2)))
+            # the following "more natural" formulation doesn't work:
+            # (forall T:thread. globally (eventually scheduled(T))) -> (globally (pc2(sk0) -> (eventually pc3(sk0))))
+	}
+
+	################################################################################
+	#
+	# The liveness to safety construction introduces the following symbols:
+	#
+	# relation   l2s_waiting
+	# relation   l2s_frozen
+	# relation   l2s_saved
+	#
+	# relation   l2s_d(X) - polymorphic relation for d
+	# relation   l2s_a(X) - polymorphic relation for a
+	#
+        # named binder: $l2s_w - for waiting on fairness constraint
+        # named binder: $l2s_s - for saved state
+	#
+	################################################################################
+
+	################################################################################
+	#
+	# Conjectures for proving liveness
+	#
+	################################################################################
+
+	object impl = {
+	    # all safety conjectures for saved state (in the future, will be autumatically added)
+	    conjecture l2s_saved -> ( ($l2s_s T. pc3(T))(T1) & ($l2s_s T. pc3(T))(T2) -> T1 = T2 )
+	    conjecture l2s_saved -> ( ($l2s_s T. pc1(T))(T) | ($l2s_s T. pc2(T))(T) | ($l2s_s T. pc3(T))(T) )
+	    conjecture l2s_saved -> ( ~($l2s_s T. pc1(T))(T) | ~($l2s_s T. pc2(T))(T) )
+	    conjecture l2s_saved -> ( ~($l2s_s T. pc1(T))(T) | ~($l2s_s T. pc3(T))(T) )
+	    conjecture l2s_saved -> ( ~($l2s_s T. pc2(T))(T) | ~($l2s_s T. pc3(T))(T) )
+	    conjecture l2s_saved -> ( ($l2s_s T,K. m(T,K))(T,K1) & ($l2s_s T,K. m(T,K))(T,K2) -> K1 = K2 )
+	    conjecture l2s_saved -> ( ($l2s_s. next_ticket) = ($l2s_s. zero) -> ($l2s_s T,K. m(T,K))(T,($l2s_s. zero)) )
+	    conjecture l2s_saved -> ( ($l2s_s. next_ticket) ~= ($l2s_s. zero) & ($l2s_s T,K. m(T,K))(T,M) -> ~($l2s_s K1,K2. le(K1,K2))(($l2s_s. next_ticket),M) )
+	    conjecture l2s_saved -> ( (($l2s_s T. pc2(T))(T) | ($l2s_s T. pc3(T))(T)) -> ($l2s_s. next_ticket) ~= ($l2s_s. zero) )
+	    conjecture l2s_saved -> ( ($l2s_s T,K. m(T,K))(T1,M) & ($l2s_s T,K. m(T,K))(T2,M) & M ~= ($l2s_s. zero) -> T1 = T2 )
+	    conjecture l2s_saved -> ( ($l2s_s T. pc2(T))(T) & ($l2s_s T,K. m(T,K))(T,M) -> ($l2s_s K1,K2. le(K1,K2))(($l2s_s. service),M) )
+	    conjecture l2s_saved -> ( ($l2s_s T. pc3(T))(T) -> ($l2s_s T,K. m(T,K))(T,($l2s_s. service)) )
+	    conjecture l2s_saved -> ( ($l2s_s K1,K2. le(K1,K2))(($l2s_s. service),($l2s_s. next_ticket)) )
+	    conjecture l2s_saved -> ( ~(~($l2s_s T. pc1(T))(T1) & ~($l2s_s T. pc1(T))(T2) & ($l2s_s T,K. m(T,K))(T1,($l2s_s. zero)) & ($l2s_s T,K. m(T,K))(T2,($l2s_s. zero)) & T1 ~= T2) )
+
+            # some things never change (maybe this should also be detected automatically)
+	    conjecture l2s_saved -> (le(X,Y) <-> ($l2s_s K1,K2. le(K1,K2))(X,Y))
+	    conjecture l2s_saved -> (zero = ($l2s_s. zero))
+	    conjecture l2s_saved -> (sk0 = ($l2s_s. sk0))
+
+	    # basic temporal information
+	    conjecture forall T:thread. globally eventually scheduled(T)
+	    conjecture eventually (pc2(sk0) & globally ~pc3(sk0))
+	    conjecture ~($l2s_w. (pc2(sk0) & globally ~pc3(sk0))) <-> (pc2(sk0) & globally ~pc3(sk0)) # TODO: why does this make sense immediately after the save point?
+
+	    # TODO: look into why these are not working:
+	    # conjecture ~(globally (pc2(sk0) -> eventually pc3(sk0)))
+	    # conjecture eventually (pc2(sk0) & globally ~pc3(sk0))
+	    # conjecture ~($l2s_w. ~(pc2(sk0) -> (eventually pc3(sk0)))) -> ~(pc2(sk0) -> (eventually pc3(sk0)))
+	    # conjecture ($l2s_w. (~(pc2(sk0) -> (eventually pc3(sk0))))) <-> (~(~(pc2(sk0) -> (eventually pc3(sk0)))))
+	    # conjecture eventually (pc2(sk0) & (globally  ~pc3(sk0)))
+	    # conjecture  ($l2s_w T. (pc2(T) & (globally ~pc3(T))))(sk0) -> ~(pc2(sk0) & (globally ~pc3(sk0)))
+	    # conjecture ~($l2s_w T. (pc2(T) & (globally ~pc3(T))))(sk0) -> (pc2(sk0) & (globally ~pc3(sk0)))
+
+            # more basic temporal properties, now in connection with monitor state
+	    conjecture l2s_frozen -> (pc2(sk0) & globally ~pc3(sk0))
+	    conjecture l2s_saved  -> (pc2(sk0) & globally ~pc3(sk0))
+	    conjecture l2s_saved  -> ($l2s_s T,K. m(T,K))(sk0,K) <-> m(sk0,K)
+	    conjecture l2s_saved  -> le( ($ l2s_s . service) , service)
+	    conjecture l2s_saved  -> le( ($ l2s_s . next_ticket) , next_ticket)
+
+	    # more properties of reachable protocol states
+	    conjecture pc1(T) & m(T,M) & M ~= zero -> ~le(service, M)
+	    conjecture forall K:ticket. ~le(next_ticket, K) & le(service, K) -> exists T:thread. m(T,K) & ~pc1(T)
+	    conjecture exists M. m(sk0, M)
+	    # and their saved counterpars (to be automatically added...)
+	    conjecture l2s_saved -> (
+		($l2s_s X. pc1(X))(T) & ($l2s_s X,Y. m(X,Y))(T,M) & M ~= ($l2s_s. zero) -> ~($l2s_s X,Y. le(X,Y))(($l2s_s. service), M)
+	    )
+	    conjecture l2s_saved -> (
+		forall KK:ticket. ~($l2s_s X,Y. le(X,Y))(($l2s_s. next_ticket), KK) & ($l2s_s X,Y. le(X,Y))(($l2s_s. service), KK) ->
+		    exists TT:thread. ($l2s_s T,K. m(T,K))(TT,KK) & ~($l2s_s T. pc1(T))(TT)
+	    )
+	    conjecture l2s_saved -> (
+		exists M. ($l2s_s T,K. m(T,K))(($l2s_s. sk0), M)
+	    )
+
+	    # l2s_d is large enough
+	    conjecture l2s_d(sk0)
+	    conjecture ~pc1(T) -> l2s_d(T)
+	    conjecture le(K,next_ticket) -> l2s_d(K)
+	    # l2s_a is large enough
+	    conjecture ~l2s_waiting -> l2s_a(sk0)
+	    conjecture ~l2s_waiting & m(T,K) & m(sk0,K0) & ~le(K0,K) & ~pc1(T) -> l2s_a(T)
+	    conjecture ~l2s_waiting & m(sk0,K0) & le(K,K0) -> l2s_a(K)
+
+	    # thread that have not been scheduled have not changed
+	    conjecture l2s_saved & ($l2s_w T. scheduled(T))(T) -> (($l2s_s T. pc1(T))(T) <-> pc1(T))
+	    conjecture l2s_saved & ($l2s_w T. scheduled(T))(T) -> (($l2s_s T. pc2(T))(T) <-> pc2(T))
+	    conjecture l2s_saved & ($l2s_w T. scheduled(T))(T) -> (($l2s_s T. pc3(T))(T) <-> pc3(T))
+	    conjecture l2s_saved & ($l2s_w T. scheduled(T))(T) -> (($l2s_s T,K. m(T,K))(T,K) <-> m(T,K))
+
+	    # the thread that must advance - the thread that had the service as its local ticket at the save point
+	    conjecture (
+	        l2s_saved &
+	        ($l2s_s T,K. m(T,K))(T,($l2s_s. service)) &
+	        ~($l2s_w X. scheduled(X))(T) &
+	        ($l2s_s T. pc2(T))(T) &
+	        m(T,K) &
+	        m(sk0,K0)
+	    ) -> (
+	        (pc1(T) & K = ($l2s_s. service)) |
+	        (pc2(T) & ~le(K,K0)) |
+	        (pc3(T) & K = ($l2s_s. service))
+	    )
+	    conjecture (
+	        l2s_saved &
+	        ($l2s_s T,K. m(T,K))(T,($l2s_s. service)) &
+	        ~($l2s_w T. scheduled(T))(T) &
+	        ($l2s_s T. pc3(T))(T) &
+	        m(T,K) &
+	        m(sk0,K0)
+	    ) -> (
+	        (pc1(T) & K = ($l2s_s. service) & ~le(service, ($l2s_s. service))) |
+	        (pc2(T) & ~le(K,K0))
+	    )
+	}
+    } with this
+}