diff --git a/examples/examples.txt b/examples/examples.txt deleted file mode 100644 index f0e5dcb15..000000000 --- a/examples/examples.txt +++ /dev/null @@ -1,11 +0,0 @@ -learning - proved, using updr -learning with count -spanning tree -leader - proved, using iupdr -client server -chord -flash -hotel -chain panda -gc copy - proved, mainly using cti -bakery diff --git a/examples/liveness/alternating_bit_protocol.ivy b/examples/liveness/alternating_bit_protocol.ivy new file mode 100644 index 000000000..b17b3bd4a --- /dev/null +++ b/examples/liveness/alternating_bit_protocol.ivy @@ -0,0 +1,488 @@ +#lang ivy1.6 +################################################################################ +# +# A basic version of alternating bit protocol with binary (1-bit) +# sequence number and FIFO channels. +# +################################################################################ + + +################################################################################ +# +# Module for axiomatizing a totally ordered set with fixed order +# +# The module includes an le relation, a minimal element (zero) and +# get_succ and get_pred actions. +# +# In this module, the order is arbitrary and fixed. +# +################################################################################ + +module total_order(carrier) = { + relation le(X:carrier,Y:carrier) # less than or equal + + axiom le(X, X) # Reflexivity + axiom le(X, Y) & le(Y, Z) -> le(X, Z) # Transitivity + axiom le(X, Y) & le(Y, X) -> X = Y # Anti-symmetry + axiom le(X, Y) | le(Y, X) # Totality + + individual zero:carrier + axiom le(zero, X) + + action get_succ(x:carrier) returns (y:carrier) = { + assume le(x,y) & x ~= y & ((le(x, Z) & x ~= Z) -> le(y, Z)) + } + + action get_pred(y:carrier) returns (x:carrier) = { + assume le(x,y) & x ~= y & ((le(x, Z) & x ~= Z) -> le(y, Z)) + } +} + +################################################################################ +# +# A module for a fifo channel +# +################################################################################ + +module fifo_channel(m_t) = { + relation le(X:m_t,Y:m_t) # partial order representing messages in + # the channel - larger messages are + # older. le(x,x) means message x is in + # the channel + + conjecture le(X, Y) & le(Y, Z) -> le(X, Z) # Transitivity + conjecture le(X, Y) & le(Y, X) -> X = Y # Anti-symmetry + conjecture le(X, Y) -> le(X, X) & le(Y, Y) # Partial reflexivity + conjecture le(X, X) & le(Y, Y) -> le(X, Y) | le(Y, X) # Partial Totality + + init ~le(X, Y) + + action send(m: m_t) = { + # insert m as a newest message + assume ~le(m, m); + le(m, m) := true; + le(m, X) := le(X,X) + } + + action receive returns (m: m_t) = { + # receive the oldest message and remove it + assume le(m, m); + assume le(m,X) -> X = m; + le(X,m) := false + } + + action drop(m:m_t) = { + # drop a message + le(X,Y) := le(X, Y) & X ~= m & Y ~= m + } +} + +object abp = { + + ################################################################################ + # + # Types, relations and functions describing state of the network + # + ################################################################################ + + ################################################################################ + # + # The protocol itself, with tracking of events for expressing + # fairness assumptions. + # + ################################################################################ + + # a totally ordered set for indices + type index_t + instantiate index : total_order(index_t) + + # an uninterpreted sort for data items + type value + individual bot:value # special bottom value + + # data messages (sent from sender to received), with a fifo channel, + # and a data item and sequence bit for every message + type data_msg_t + instantiate data_msg : fifo_channel(data_msg_t) + individual d(D:data_msg_t) : value # immutable + relation dbit(D:data_msg_t) # immutable + + # ack messages (sent from receiver to sender), with a fifo channel and + # a sequence number bit for every message. + type ack_msg_t + instantiate ack_msg : fifo_channel(ack_msg_t) + relation abit(A:ack_msg_t) # immutable + + # sender array and receiver array + individual sender_array(I:index_t) : value + individual receiver_array(I:index_t) : value + init sender_array(I) = bot + init receiver_array(I) = bot + + # sender index and receiver index + individual sender_i:index_t + init sender_i = index.zero + individual sender_gen_i:index_t + init sender_gen_i = index.zero + individual receiver_i:index_t + init receiver_i = index.zero + + # sender and receiver bits, initially 0 (false) + relation sender_bit + init ~sender_bit + relation receiver_bit + init ~receiver_bit + + # state for encoding the fairness assumptions + relation sender_scheduled + relation receiver_scheduled + relation data_sent + relation data_received + relation ack_sent + relation ack_received + init ~sender_scheduled + init ~receiver_scheduled + init ~data_sent + init ~data_received + init ~ack_sent + init ~ack_received + + ################################################################################ + # + # Protocol actions + # + ################################################################################ + + action reset_fairness = { + sender_scheduled := false; + receiver_scheduled := false; + data_sent := false; + data_received := false; + ack_sent := false; + ack_received := false; + } + + action gen_data(v:value) = { + call reset_fairness; + assume v ~= bot; + sender_array(sender_gen_i) := v; + sender_gen_i := index.get_succ(sender_gen_i); + } + + action sender_send_data(m:data_msg_t, a:ack_msg_t) = { + call reset_fairness; + sender_scheduled := true; + if (sender_array(sender_i) ~= bot) { + assume d(m) = sender_array(sender_i); + assume dbit(m) <-> sender_bit; + call data_msg.send(m); + data_sent := true; + }; + } + + action sender_receive_ack(m:data_msg_t, a:ack_msg_t) = { + call reset_fairness; + ack_received := true; + a := ack_msg.receive(); + if abit(a) <-> sender_bit { + sender_bit := ~sender_bit; + sender_i := index.get_succ(sender_i) + }; + } + + action receiver_receive_data(m:data_msg_t, a:ack_msg_t) = { + call reset_fairness; + data_received := true; + m := data_msg.receive(); + if dbit(m) <-> receiver_bit { + # flip receiver bit, append to receiver array + receiver_bit := ~receiver_bit; + receiver_array(receiver_i) := d(m); + receiver_i := index.get_succ(receiver_i) + }; + } + + action receiver_send_ack(m:data_msg_t, a:ack_msg_t) = { + call reset_fairness; + receiver_scheduled := true; + # send ack with ~receiver_bit + assume abit(a) <-> ~receiver_bit; + call ack_msg.send(a); + ack_sent := true; + } + + action data_msg_drop(m:data_msg_t, a:ack_msg_t) = { + call reset_fairness; + call data_msg.drop(m); + } + + action ack_msg_drop(m:data_msg_t, a:ack_msg_t) = { + call reset_fairness; + call ack_msg.drop(a); + } + + export gen_data + export sender_send_data + export sender_receive_ack + export receiver_receive_data + export receiver_send_ack + export data_msg_drop + export ack_msg_drop + + ################################################################################ + # + # Conjectures for proving safety (also helps for liveness) + # + ################################################################################ + + # safety - receiver array has values from sender array for all received indices + conjecture receiver_array(I) ~= bot -> receiver_array(I) = sender_array(I) + + # inductive invariant for proving safety + + conjecture index.le(sender_gen_i, I) <-> sender_array(I) = bot + conjecture index.le(receiver_i, I) <-> receiver_array(I) = bot + conjecture index.le(sender_i, sender_gen_i) + + conjecture ~sender_bit & ~receiver_bit & ack_msg.le(A,A) -> abit(A) + conjecture ~sender_bit & ~receiver_bit & data_msg.le(M1,M2) -> ~(dbit(M1) & ~dbit(M2)) + + conjecture sender_bit & receiver_bit & ack_msg.le(A,A) -> ~abit(A) + conjecture sender_bit & receiver_bit & data_msg.le(M1,M2) -> ~(~dbit(M1) & dbit(M2)) + + conjecture ~sender_bit & receiver_bit & data_msg.le(M,M) -> ~dbit(M) + conjecture ~sender_bit & receiver_bit & ack_msg.le(A1,A2) -> ~(abit(A1) & ~abit(A2)) + + conjecture sender_bit & ~receiver_bit & data_msg.le(M,M) -> dbit(M) + conjecture sender_bit & ~receiver_bit & ack_msg.le(A1,A2) -> ~(~abit(A1) & abit(A2)) + + conjecture (sender_bit <-> receiver_bit) -> sender_i = receiver_i + conjecture (sender_bit <-> ~receiver_bit) -> ( + # receiver_i = sender_i + 1 + ~index.le(receiver_i, sender_i) & + (forall I. ~index.le(I,sender_i) -> index.le(receiver_i,I)) + ) + + conjecture data_msg.le(M,M) & (dbit(M) <-> sender_bit) -> ~index.le(sender_gen_i, sender_i) + conjecture data_msg.le(M,M) & (dbit(M) <-> sender_bit) -> d(M) = sender_array(sender_i) + conjecture data_msg.le(M,M) -> d(M) ~= bot + + conjecture ack_msg.le(A,A) & (abit(A) <-> sender_bit) -> ~index.le(receiver_i,sender_i) + conjecture ack_msg.le(A,A) & (abit(A) <-> sender_bit) -> receiver_array(sender_i) = sender_array(sender_i) + conjecture ack_msg.le(A,A) & (abit(A) <-> sender_bit) -> receiver_array(sender_i) ~= bot + + ################################################################################ + # + # Temporal property and its proof + # + ################################################################################ + + isolate tp1 = { + + ################################################################################ + # + # Liveness proof + # + # The property to prove is: + # ( + # (globally eventually sender_scheduled) & # scheduling fairness + # (globally eventually receiver_scheduled) & # scheduling fairness + # ((globally eventually data_sent) -> (globally eventually data_received)) # data channel fairness + # ((globally eventually ack_sent) -> (globally eventually ack_received)) # ack channel fairness + # ) -> (forall I. globally (sender_array(I) ~= bot -> eventually (receiver_array(I) ~= bot))) + # + # The set A of formulas containts the following formulas (and their subformulas): + # 1. the property + # 2. eventually globally ~sender_bit & ~receiver_bit + # 3. eventually globally ~sender_bit & receiver_bit + # 4. eventually globally sender_bit & ~receiver_bit + # 5. eventually globally sender_bit & receiver_bit + # + # We also use "witness constants" for the following formula: + # ~ globally (sender_array(I) ~= bot -> eventually receiver_array(I) ~= bot) + # + ################################################################################ + + individual sk0:index_t # witness for the formula (exists I. ~ globally (sender_array(I) ~= bot -> (eventually receiver_array(I) ~= bot))) + + object spec = { + temporal property [liveness] ( + ((exists I. ~ globally (sender_array(I) ~= bot -> (eventually receiver_array(I) ~= bot))) -> + (~ globally (sender_array(sk0) ~= bot -> (eventually receiver_array(sk0) ~= bot)))) & + + (globally eventually sender_scheduled) & # scheduling fairness + (globally eventually receiver_scheduled) & # scheduling fairness + ((globally eventually data_sent) -> (globally eventually data_received)) & # data channel fairness + ((globally eventually ack_sent) -> (globally eventually ack_received)) # ack channel fairness + ) -> (forall I. globally (sender_array(I) ~= bot -> eventually (receiver_array(I) ~= bot))) + } + + ################################################################################ + # + # Conjectures for proving liveness + # + ################################################################################ + + object impl = { + # all safety conjectures for saved state (in the future, will be autumatically added) + conjecture l2s_saved -> ( ($l2s_s X. receiver_array(X))(I) ~= ($l2s_s. bot) -> ($l2s_s X. receiver_array(X))(I) = ($l2s_s X. sender_array(X))(I) ) + conjecture l2s_saved -> ( ($l2s_s X,Y. index.le(X,Y))(($l2s_s. sender_gen_i), I) <-> ($l2s_s X. sender_array(X))(I) = ($l2s_s. bot) ) + conjecture l2s_saved -> ( ($l2s_s X,Y. index.le(X,Y))(($l2s_s. receiver_i), I) <-> ($l2s_s X. receiver_array(X))(I) = ($l2s_s. bot) ) + conjecture l2s_saved -> ( ($l2s_s X,Y. index.le(X,Y))(($l2s_s. sender_i), ($l2s_s. sender_gen_i)) ) + conjecture l2s_saved -> ( ~($l2s_s. sender_bit) & ~($l2s_s. receiver_bit) & ($l2s_s X,Y. ack_msg.le(X,Y))(A,A) -> ($l2s_s X. abit(X))(A) ) + conjecture l2s_saved -> ( ~($l2s_s. sender_bit) & ~($l2s_s. receiver_bit) & ($l2s_s X,Y. data_msg.le(X,Y))(M1,M2) -> ~(($l2s_s X. dbit(X))(M1) & ~($l2s_s X. dbit(X))(M2)) ) + conjecture l2s_saved -> ( ($l2s_s. sender_bit) & ($l2s_s. receiver_bit) & ($l2s_s X,Y. ack_msg.le(X,Y))(A,A) -> ~($l2s_s X. abit(X))(A) ) + conjecture l2s_saved -> ( ($l2s_s. sender_bit) & ($l2s_s. receiver_bit) & ($l2s_s X,Y. data_msg.le(X,Y))(M1,M2) -> ~(~($l2s_s X. dbit(X))(M1) & ($l2s_s X. dbit(X))(M2)) ) + conjecture l2s_saved -> ( ~($l2s_s. sender_bit) & ($l2s_s. receiver_bit) & ($l2s_s X,Y. data_msg.le(X,Y))(M,M) -> ~($l2s_s X. dbit(X))(M) ) + conjecture l2s_saved -> ( ~($l2s_s. sender_bit) & ($l2s_s. receiver_bit) & ($l2s_s X,Y. ack_msg.le(X,Y))(A1,A2) -> ~(($l2s_s X. abit(X))(A1) & ~($l2s_s X. abit(X))(A2)) ) + conjecture l2s_saved -> ( ($l2s_s. sender_bit) & ~($l2s_s. receiver_bit) & ($l2s_s X,Y. data_msg.le(X,Y))(M,M) -> ($l2s_s X. dbit(X))(M) ) + conjecture l2s_saved -> ( ($l2s_s. sender_bit) & ~($l2s_s. receiver_bit) & ($l2s_s X,Y. ack_msg.le(X,Y))(A1,A2) -> ~(~($l2s_s X. abit(X))(A1) & ($l2s_s X. abit(X))(A2)) ) + conjecture l2s_saved -> ( (($l2s_s. sender_bit) <-> ($l2s_s. receiver_bit)) -> ($l2s_s. sender_i) = ($l2s_s. receiver_i) ) + conjecture l2s_saved -> ( (($l2s_s. sender_bit) <-> ~($l2s_s. receiver_bit)) -> (~($l2s_s X,Y. index.le(X,Y))(($l2s_s. receiver_i), ($l2s_s. sender_i)) & (forall I. ~($l2s_s X,Y. index.le(X,Y))(I,($l2s_s. sender_i)) -> ($l2s_s X,Y. index.le(X,Y))(($l2s_s. receiver_i),I))) ) + conjecture l2s_saved -> ( ($l2s_s X,Y. data_msg.le(X,Y))(M,M) & (($l2s_s X. dbit(X))(M) <-> ($l2s_s. sender_bit)) -> ~($l2s_s X,Y. index.le(X,Y))(($l2s_s. sender_gen_i), ($l2s_s. sender_i)) ) + conjecture l2s_saved -> ( ($l2s_s X,Y. data_msg.le(X,Y))(M,M) & (($l2s_s X. dbit(X))(M) <-> ($l2s_s. sender_bit)) -> ($l2s_s X. d(X))(M) = ($l2s_s X. sender_array(X))(($l2s_s. sender_i)) ) + conjecture l2s_saved -> ( ($l2s_s X,Y. data_msg.le(X,Y))(M,M) -> ($l2s_s X. d(X))(M) ~= ($l2s_s. bot) ) + conjecture l2s_saved -> ( ($l2s_s X,Y. ack_msg.le(X,Y))(A,A) & (($l2s_s X. abit(X))(A) <-> ($l2s_s. sender_bit)) -> ~($l2s_s X,Y. index.le(X,Y))(($l2s_s. receiver_i),($l2s_s. sender_i)) ) + conjecture l2s_saved -> ( ($l2s_s X,Y. ack_msg.le(X,Y))(A,A) & (($l2s_s X. abit(X))(A) <-> ($l2s_s. sender_bit)) -> ($l2s_s X. receiver_array(X))(($l2s_s. sender_i)) = ($l2s_s X. sender_array(X))(($l2s_s. sender_i)) ) + conjecture l2s_saved -> ( ($l2s_s X,Y. ack_msg.le(X,Y))(A,A) & (($l2s_s X. abit(X))(A) <-> ($l2s_s. sender_bit)) -> ($l2s_s X. receiver_array(X))(($l2s_s. sender_i)) ~= ($l2s_s. bot) ) + + # some things never change (maybe this should also be detected automatically) + conjecture l2s_saved -> (index.le(X,Y) <-> ($l2s_s X,Y. index.le(X,Y))(X,Y)) + conjecture l2s_saved -> (index.zero = ($l2s_s. index.zero)) + conjecture l2s_saved -> (abit(X) <-> ($l2s_s X. abit(X))(X)) + conjecture l2s_saved -> (dbit(X) <-> ($l2s_s X. dbit(X))(X)) + conjecture l2s_saved -> (d(X) = ($l2s_s X. d(X))(X)) + conjecture l2s_saved -> (sk0 = ($l2s_s. sk0)) + + # basic temporal information + conjecture globally eventually sender_scheduled + conjecture globally eventually receiver_scheduled + conjecture (globally eventually data_sent) -> (globally eventually data_received) + conjecture (globally eventually ack_sent) -> (globally eventually ack_received) + + # properties of sk0 + conjecture ~globally (sender_array(sk0) ~= bot -> (eventually receiver_array(sk0) ~= bot)) + conjecture ~($l2s_w. ~(sender_array(sk0) ~= bot -> (eventually receiver_array(sk0) ~= bot))) -> ~(sender_array(sk0) ~= bot -> (eventually receiver_array(sk0) ~= bot)) + conjecture ~l2s_waiting -> sender_array(sk0) ~= bot + conjecture ~l2s_waiting -> (~eventually receiver_array(sk0) ~= bot) + conjecture ~l2s_waiting -> receiver_array(sk0) = bot + # interestingly, this is not provable in the l2s_waiting state: + # conjecture receiver_array(sk0) = bot + + # basic use of temporal prophecy formulas + conjecture (eventually globally (~sender_bit & ~receiver_bit)) & (~l2s_waiting | ~($l2s_w. globally (~sender_bit & ~receiver_bit))) -> globally (~sender_bit & ~receiver_bit) + conjecture (eventually globally (~sender_bit & receiver_bit)) & (~l2s_waiting | ~($l2s_w. globally (~sender_bit & receiver_bit))) -> globally (~sender_bit & receiver_bit) + conjecture (eventually globally ( sender_bit & ~receiver_bit)) & (~l2s_waiting | ~($l2s_w. globally ( sender_bit & ~receiver_bit))) -> globally ( sender_bit & ~receiver_bit) + conjecture (eventually globally ( sender_bit & receiver_bit)) & (~l2s_waiting | ~($l2s_w. globally ( sender_bit & receiver_bit))) -> globally ( sender_bit & receiver_bit) + + # l2s_d is large enough + conjecture index.le(I,sender_gen_i) -> l2s_d(I) + conjecture data_msg.le(M,M) -> l2s_d(M) + conjecture ack_msg.le(A,A) -> l2s_d(A) + # l2s_a is large enough + conjecture ~l2s_waiting -> ( index.le(I,sk0) -> l2s_a(I) ) + conjecture ~l2s_waiting & ( + (globally (~sender_bit & ~receiver_bit)) | + (globally (~sender_bit & receiver_bit)) | + (globally ( sender_bit & ~receiver_bit)) | + (globally ( sender_bit & receiver_bit)) + ) -> ( data_msg.le(M,M) & (dbit(M) <-> ~sender_bit) -> l2s_a(M) ) + conjecture ~l2s_waiting & ( + (globally (~sender_bit & ~receiver_bit)) | + (globally (~sender_bit & receiver_bit)) | + (globally ( sender_bit & ~receiver_bit)) | + (globally ( sender_bit & receiver_bit)) + ) -> ( ack_msg.le(A,A) & (abit(A) <-> receiver_bit) -> l2s_a(A) ) + + + # more properties of reachable protocol states (but only in ~l2s_waiting) + conjecture ~l2s_waiting -> index.le(sender_i, sk0) + conjecture ~l2s_waiting -> index.le(receiver_i, sk0) + # and their saved state counterparts + conjecture l2s_saved -> ($l2s_s X,Y. index.le(X,Y))(($l2s_s. sender_i), ($l2s_s. sk0)) + conjecture l2s_saved -> ($l2s_s X,Y. index.le(X,Y))(($l2s_s. receiver_i), ($l2s_s. sk0)) + + # relating current state and saved state + conjecture l2s_saved -> index.le(($l2s_s. sender_i), sender_i) + conjecture l2s_saved -> index.le(($l2s_s. receiver_i), receiver_i) + conjecture l2s_saved & ( + (globally (~sender_bit & ~receiver_bit)) | + (globally (~sender_bit & receiver_bit)) | + (globally ( sender_bit & ~receiver_bit)) | + (globally ( sender_bit & receiver_bit)) + ) -> ( + ( sender_bit <-> ($l2s_s. sender_bit) ) & + ( receiver_bit <-> ($l2s_s. receiver_bit) ) & + ( sender_i = ($l2s_s. sender_i) ) & + ( receiver_i = ($l2s_s. receiver_i) ) + ) + conjecture l2s_saved & ( + (globally (~sender_bit & ~receiver_bit)) | + (globally (~sender_bit & receiver_bit)) | + (globally ( sender_bit & ~receiver_bit)) | + (globally ( sender_bit & receiver_bit)) + ) -> ( + data_msg.le(M,M) & (dbit(M) <-> ~sender_bit) -> ($l2s_s X,Y. data_msg.le(X,Y))(M,M) + ) + conjecture l2s_saved & ( + (globally (~sender_bit & ~receiver_bit)) | + (globally (~sender_bit & receiver_bit)) | + (globally ( sender_bit & ~receiver_bit)) | + (globally ( sender_bit & receiver_bit)) + ) -> ( + ack_msg.le(A,A) & (abit(A) <-> receiver_bit) -> ($l2s_s X,Y. ack_msg.le(X,Y))(A,A) + ) + conjecture l2s_saved & (sender_bit <-> ~($l2s_s. sender_bit)) -> sender_i ~= ($l2s_s. sender_i) + conjecture l2s_saved & (receiver_bit <-> ~($l2s_s. receiver_bit)) -> receiver_i ~= ($l2s_s. receiver_i) + + # proof that messages are infinitely often sent and received + conjecture ~(globally eventually data_sent) & (~l2s_waiting | ~($l2s_w. globally ~data_sent)) -> globally ~data_sent + conjecture ~(globally eventually ack_sent) & (~l2s_waiting | ~($l2s_w. globally ~ack_sent)) -> globally ~ack_sent + conjecture l2s_saved -> (($l2s_s. globally ~data_sent) -> globally ~data_sent) + conjecture l2s_saved -> (($l2s_s. globally ~ack_sent) -> globally ~ack_sent) + conjecture l2s_saved & ~($l2s_w. sender_scheduled) -> ~($l2s_s. globally ~data_sent) + conjecture l2s_saved & ~($l2s_w. receiver_scheduled) -> ~($l2s_s. globally ~ack_sent) + + # the messages that exist and show the difference between current state and saved state + conjecture l2s_saved & ( + (globally (~sender_bit & ~receiver_bit)) | + (globally (~sender_bit & receiver_bit)) | + (globally ( sender_bit & ~receiver_bit)) | + (globally ( sender_bit & receiver_bit)) + ) & ~($l2s_w. data_received) & ~(globally ~data_sent) & (($l2s_s. sender_bit) <-> ($l2s_s. receiver_bit)) -> + exists M:data_msg_t. l2s_a(M) & ~data_msg.le(M,M) & ($l2s_s X,Y. data_msg.le(X,Y))(M,M) & (dbit(M) <-> ~receiver_bit) + + conjecture l2s_saved & ( + (globally (~sender_bit & ~receiver_bit)) | + (globally (~sender_bit & receiver_bit)) | + (globally ( sender_bit & ~receiver_bit)) | + (globally ( sender_bit & receiver_bit)) + ) & ~($l2s_w. ack_received) & ~(globally ~ack_sent) & (($l2s_s. sender_bit) <-> ~($l2s_s. receiver_bit)) -> + exists A:ack_msg_t. l2s_a(A) & ~ack_msg.le(A,A) & ($l2s_s X,Y. ack_msg.le(X,Y))(A,A) & (abit(A) <-> ~sender_bit) + + # index shows the difference between current state and + # saved state (just the same conjecture 4 times, for the + # possible valuations of saved sender and receiver bits + conjecture l2s_saved & + ~(globally (~sender_bit & ~receiver_bit)) & + ~($l2s_s. sender_bit) & ~($l2s_s. receiver_bit) & + ~($l2s_w. ~(~sender_bit & ~receiver_bit)) + -> ( sender_i ~= ($l2s_s. sender_i) | receiver_i ~= ($l2s_s. receiver_i) ) + conjecture l2s_saved & + ~(globally (~sender_bit & receiver_bit)) & + ~($l2s_s. sender_bit) & ($l2s_s. receiver_bit) & + ~($l2s_w. ~(~sender_bit & receiver_bit)) + -> ( sender_i ~= ($l2s_s. sender_i) | receiver_i ~= ($l2s_s. receiver_i) ) + conjecture l2s_saved & + ~(globally ( sender_bit & ~receiver_bit)) & + ($l2s_s. sender_bit) & ~($l2s_s. receiver_bit) & + ~($l2s_w. ~( sender_bit & ~receiver_bit)) + -> ( sender_i ~= ($l2s_s. sender_i) | receiver_i ~= ($l2s_s. receiver_i) ) + conjecture l2s_saved & + ~(globally ( sender_bit & receiver_bit)) & + ($l2s_s. sender_bit) & ($l2s_s. receiver_bit) & + ~($l2s_w. ~( sender_bit & receiver_bit)) + -> ( sender_i ~= ($l2s_s. sender_i) | receiver_i ~= ($l2s_s. receiver_i) ) + } + } with this +} diff --git a/examples/liveness/ticket.ivy b/examples/liveness/ticket.ivy new file mode 100644 index 000000000..1d61552a5 --- /dev/null +++ b/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 +} diff --git a/examples/liveness/ticket_nested.ivy b/examples/liveness/ticket_nested.ivy new file mode 100644 index 000000000..895f631c7 --- /dev/null +++ b/examples/liveness/ticket_nested.ivy @@ -0,0 +1,330 @@ +#lang ivy1.6 + +################################################################################ +# A liveness proof of the nested 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 c(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 c(T,K) <-> K = zero + init ~scheduled(T) + + ################################################################################ + # + # Protocol actions + # + ################################################################################ + + action step12(t:thread,k1:ticket, k2:ticket) = { + assume pc1(t); + assume k1 = next_ticket; + assume ~le(k2,k1) & forall Z:ticket. ~le(Z,k1) -> le(k2,Z); + m(t,K) := K = k1; + next_ticket := k2; + 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, k2:ticket) = { + assume pc2(t); + assume m(t,k1); + assume le(k1,service); + pc2(t) := false; + pc3(t) := true; + c(t,K) := K = next_ticket; # TODO: change this to k2, and change the update of d to account for a downward finite total order + scheduled(T) := T = t; + } + + action step33(t:thread, k1:ticket, k2:ticket) = { + assume pc3(t); + assume c(t,k2); + assume ~le(k2,k1) & forall Z:ticket. ~le(Z,k1) -> le(k2,Z); + c(t,K) := K = k1; + # stay in pc3 + scheduled(T) := T = t; + } + + action step31(t:thread, k1:ticket, k2:ticket) = { + assume pc3(t); + assume c(t,zero); + assume k1 = service; + assume ~le(k2,k1) & forall Z:ticket. ~le(Z,k1) -> le(k2,Z); + service := k2; + pc3(t) := false; + pc1(t) := true; + scheduled(T) := T = t; + } + + export step12 + export step22 + export step23 + export step33 + 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 + conjecture c(T,K1) & c(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 = { + + ################################################################################ + # + # Liveness proof + # + # The property to prove is: + # (forall T. globally eventually scheduled(T)) -> (forall T. globally (pc2(T) -> eventually pc3(T))) + # + # The set A of formulas containts the following formulas (and their subformulas): + # the property: (forall T. globally ~ globally ~scheduled(T)) -> (forall T. globally (~pc2(T) | ~ globally ~pc3(T))) + # additional formula: forall T. globally ~globally pc3(T) + # + # We also use "witness constants" for the following formulas: + # + # + ################################################################################ + + + individual sk0:thread # witness for the formula (exists T0. ~(globally ~(pc2(T0) & globally ~pc3(T0)))) + individual sk1:thread # witness for the formula (exists T1. ~(globally ~(globally pc3(T1)))) + + object spec = { + temporal property [nonstravation] ( + ((exists T0. ~(globally ~(pc2(T0) & globally ~pc3(T0)))) -> ~(globally ~(pc2(sk0) & globally ~pc3(sk0)))) & + ((exists T1. ~(globally ~(globally pc3(T1)))) -> (~(globally ~(globally pc3(sk1))))) & + (forall T2. globally (eventually scheduled(T2))) + ) -> (forall T3. globally ~(pc2(T3) & globally ~pc3(T3))) + } + + ################################################################################ + # + # 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 T,K. c(T,K))(T,K1) & ($l2s_s T,K. c(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)) + conjecture l2s_saved -> (sk1 = ($l2s_s. sk1)) + + # basic temporal information + conjecture forall T:thread. globally eventually scheduled(T) + conjecture ~(globally ~(pc2(sk0) & globally ~pc3(sk0))) + conjecture ~($l2s_w. (pc2(sk0) & globally ~pc3(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) + + # temporal information regarding sk1 + conjecture ~(globally ~(globally pc3(sk1))) | (forall T. globally (~globally pc3(T))) + conjecture ~(globally ~(globally pc3(sk1))) | (forall T. (~globally pc3(T))) + conjecture (~($l2s_w. (globally pc3(sk1)))) -> ( + (globally ~(globally pc3(sk1))) | + (globally pc3(sk1)) + ) + conjecture ~(globally ~(globally pc3(sk1))) & ~l2s_waiting -> globally pc3(sk1) + # more information about sk1 + conjecture exists K. c(sk1,K) + conjecture l2s_saved -> exists K. ($l2s_s T,K. c(T,K))(sk1,K) + conjecture (globally pc3(sk1)) & l2s_saved & c(sk1,K1) & ($l2s_s T,K. c(T,K))(sk1,K2) -> le(K1,K2) + conjecture (globally pc3(sk1)) & l2s_saved & c(sk1,K1) & ($l2s_s T,K. c(T,K))(sk1,K2) & ~($l2s_w X. scheduled(X))(sk1) -> K1 ~= K2 + + # 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 l2s_d(sk1) + conjecture ~pc1(T) -> l2s_d(T) + conjecture le(K,next_ticket) -> l2s_d(K) + conjecture c(sk1,K0) & le(K,K0) -> l2s_d(K) + # l2s_a is large enough + conjecture ~l2s_waiting -> l2s_a(sk0) + conjecture ~l2s_waiting -> l2s_a(sk1) + 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) + conjecture ~l2s_waiting & (globally pc3(sk1)) & c(sk1,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)) + conjecture l2s_saved & ($l2s_w T. scheduled(T))(T) -> (($l2s_s T,K. c(T,K))(T,K) <-> c(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_s T. pc3(T))(T) & + m(T,K) & + m(sk0,K0) + ) -> ( + (pc3(T) & K = ($l2s_s. service) & K = service) | + (pc1(T) & K = ($l2s_s. service) & ~le(service, ($l2s_s. service))) | + (pc2(T) & ~le(K,K0)) + ) + conjecture ( + l2s_saved & + ($l2s_s T,K. m(T,K))(T,($l2s_s. service)) & + ($l2s_s T. pc3(T))(T) & + m(T,K) & + m(sk0,K0) & + ~($l2s_w T. ~pc3(T))(T) & + ~(globally pc3(T)) + ) -> ( + (pc1(T) & K = ($l2s_s. service) & ~le(service, ($l2s_s. service))) | + (pc2(T) & ~le(K,K0)) + ) + } + } with this +} diff --git a/examples/pldi16/abstract_paxos_9_proof_induction.ivy b/examples/pldi16/abstract_paxos_9_proof_induction.ivy new file mode 100644 index 000000000..3684a8968 --- /dev/null +++ b/examples/pldi16/abstract_paxos_9_proof_induction.ivy @@ -0,0 +1,242 @@ +#lang ivy1.3 + +################################################################################ +# +# Modules that should probably come from a standard library +# +################################################################################ + + +################################################################################ +# +# Module describing an acyclic partial function. The function is built by +# calling the "set" action. This has preconditions that enforce the required +# invariants. The function can be accessed using "dom" to query if an element is +# in the domain of the function, and "get" to get its value. The "get" action +# has a precondition that the given element must be in the domain. +# +# Because of the invariant that the relation re construct by "set" is an acyclic +# partial function, we can represent it by its transitive closure "tc", while +# remainin in EPR. +# +################################################################################ + +module acyclic_partial_function(carrier) = { + relation tc(X:carrier,Y:carrier) # transitive closure of the function + relation f(X:carrier, Y:carrier) # the function itself, but this is just an under-approximation + + # Conjectures that ensure that tc really describes the transitive closure + # of an acyclic partial function. + # These conjectures form part of the safety property. + conjecture tc(X,X) # Reflexivity + conjecture tc(X, Y) & tc(Y, Z) -> tc(X, Z) # Transitivity + conjecture tc(X, Y) & tc(Y, X) -> X = Y # Anti-symmetry + conjecture tc(X, Y) & tc(X, Z) -> (tc(Y, Z) | tc(Z, Y)) # Semi-linearity + + # conjecture about f (we can't have the iff) + conjecture f(X,Y) -> tc(X,Y) & X ~= Y & ((tc(X, Z) & X ~= Z) -> tc(Y, Z)) + conjecture f(X,Y1) & f(X,Y2) -> Y1 = Y2 + + # initially empty + init (tc(X,Y) <-> X = Y) + init ~f(X,Y) + + action set(x:carrier,y:carrier) = { + tc(X, Y) := tc(X, Y) | (tc(X, x) & tc(y, Y)); + f(x, Y) := Y = y + } + + action get(x:carrier) returns (y:carrier) = { + #assume tc(x,y) & x ~= y & ((tc(x, Z) & x ~= Z) -> tc(y, Z)) + assume f(x,y) + } +} + +################################################################################ +# +# 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 state of the network +# +################################################################################ + +type node +type value +type quorum +type round + +individual first : round +individual none: round +relation le(X:round, Y:round) +instantiate total_order(le) +axiom le(none, X) +axiom ~le(first, none) +axiom ~le(X, none) -> le(first, X) + +relation member(N:node, Q:quorum) +# forall Q1 Q2 exists N. member(N, Q1) & member(N, Q2) +individual quorum_intersection(Q1:quorum, Q2:quorum) : node # a Skolem function +axiom member(quorum_intersection(Q1, Q2), Q1) +axiom member(quorum_intersection(Q1, Q2), Q2) + +# ghost functions for recording the existence of quorums and voter nodes +individual quorum_of_proposal(R:round) : quorum +individual quorum_of_decision(R:round) : quorum + +relation proposal(R1:round, V:value) # 2a +instantiate p_round : acyclic_partial_function(round) # a proposal round ghost partial function modeled by its transitive closure + +relation vote(N:node, R:round, V:value) # 2b +relation decision(R:round, V:value) # got 2b from a quorum +relation rnd(N:node, R:round) # rnd(n,r) means node n sent 1b to round r + + +init ~proposal(R,V) +init ~vote(N,R,V) +init ~decision(R,V) +init rnd(N, R) <-> R = first + +action cast_vote = { + # phase 2b + local n:node, v:value, r:round { + assume r ~= none; + assume rnd(n, r) & (rnd(n,R) -> le(R,r)); + assume proposal(r, v); + vote(n, r, v) := true + } +} + +action decide = { + # get 2b from a quorum + local r:round, v:value, q:quorum { + assume r ~= none; + assume member(N, q) -> vote(N, r, v); + quorum_of_decision(r) := q; + decision(r, v) := true + } +} + +action join_round = { + # receive 1a and answer with 1b + local n:node, r:round { + assume r ~= none; + assume rnd(n,R) -> ~le(r,R); + # node n joins r2: + rnd(n, r) := true + } +} + +action propose = { + local r:round, v:value, q:quorum, pr:round, voter:node { + assume r ~= none; + assume ~proposal(r,V); + assume p_round.tc(r,R) -> r = R; # this is actually not so good that we need this here + assume member(N, q) -> rnd(N,r); + + # find the latest vote in the quorum before round r + if ~(member(VOTER:node, q) & vote(VOTER:node, PR:round, V:value) & ~le(r, PR:round)) { + assume pr = none + } else { + assume member(voter, q) & vote(voter, pr, v) & ~le(r, pr); + assume member(VOTER ,q) & vote(VOTER, PR, V) & ~le(r, PR) -> le(PR, pr) + }; + proposal(r, v) := true; + quorum_of_proposal(r) := q; + call p_round.set(r, pr) + } +} + +export cast_vote +export join_round +export decide +export propose + +# Bogus conjectures to test the system + +# # counter-example in 7 steps: +# conjecture ~( +# R1 ~= R2 & +# decision(R1,V1) & +# decision(R2,V2) +# ) + +# # counter-example in 11 steps: +# conjecture ~( +# R1 ~= R2 & R3 ~= R2 & R1 ~= R3 & +# decision(R1,V1) & +# decision(R2,V2) & +# decision(R3,V3) +# ) + +# safety property: +conjecture ( + decision(R1,V1) & + decision(R2,V2) +) -> V1 = V2 + +# a proposal in round comes from a quorum: +conjecture proposal(R,V) & member(N, quorum_of_proposal(R)) -> rnd(N, R) + +# proposals are unique per round +conjecture proposal(R,V1) & proposal(R,V2) -> V1 = V2 + +# decisions come from quorums of votes: +conjecture decision(R,V) & member(N, quorum_of_decision(R)) -> vote(N,R,V) + +# only vote for joined rounds +conjecture vote(N,R,V) -> rnd(N,R) + +# only vote for proposed values +conjecture vote(N,R,V) -> proposal(R,V) + +# decisions are respected by future proposals +# conjecture le(R1, R2) & decision(R1,V1) & proposal(R2,V2) -> V1 = V2 +# +# decisions are respected by future proposals +conjecture le(R1, R2) & decision(R1,V1) & proposal(R2,V2) -> V1 = V2 + +# need to apply induction to obtain the minimal R2 that violates the +# above conjecture, and then obtain its p_round.f +individual min_bad_r1:round +individual min_bad_r2:round +individual min_bad_v1:value +individual min_bad_v2:value +individual min_bad_f:round +axiom ( + # if R2 is a bad round w.r.t. R1, then min_bad_r2 is bad w.r.t. min_bad_r1, and R2 >= min_bad_r2 + (le(R1, R2) & decision(R1,V1) & proposal(R2,V2) & V1 ~= V2) -> ( + (le(min_bad_r1, min_bad_r2) & decision(min_bad_r1,min_bad_v1) & proposal(min_bad_r2,min_bad_v2) & min_bad_v1 ~= min_bad_v2) & + le(min_bad_r2, R2) + ) +) +# manually instantiate an AE axiom for min_bad_r2 +axiom p_round.tc(min_bad_r2,R) & min_bad_r2 ~= R -> p_round.f(min_bad_r2, min_bad_f) + +# properties of none +conjecture ~proposal(none,V) +conjecture ~rnd(N,none) +conjecture ~vote(N,none,V) +conjecture ~decision(none,V) + +# properties of p_round.tc +conjecture p_round.tc(R1,R2) -> le(R2,R1) +conjecture proposal(R,V) -> p_round.tc(R,none) +conjecture proposal(R1,V1) & proposal(R2,V2) & p_round.tc(R1,R2) -> V1 = V2 +conjecture ~(p_round.tc(R3,R2) & proposal(R3,V0) & ~proposal(R2,V0) & R2 ~= none) + +# properties of p_round.f +# we want to say that p_round is the last voted round, but we have to use p_round.f +conjecture ~le(R3,R2) & proposal(R3,V3) & member(N,quorum_of_proposal(R3)) & vote(N,R2,V2) & p_round.f(R3,R1) -> le(R2,R1) +# now all we have to say but can't is proposal(R,V) -> exists PR. p_round.f(R,PR) diff --git a/examples/pldi16/alternating_bit_protocol.ivy b/examples/pldi16/alternating_bit_protocol.ivy new file mode 100644 index 000000000..9401dd35f --- /dev/null +++ b/examples/pldi16/alternating_bit_protocol.ivy @@ -0,0 +1,205 @@ +#lang ivy1.3 + +# +# A basic version of alternating bit protocol with binary (1-bit) +# sequence number and FIFO channels. +# + +################################################################################ +# +# Module for axiomatizing a totally ordered set with fixed order +# +# The module includes an le relation, a minimal element (zero) and +# get_succ and get_pred actions. +# +# In this module, the order is arbitrary and fixed. +# +################################################################################ + +module total_order(carrier) = { + relation le(X:carrier,Y:carrier) # less than or equal + + axiom le(X, X) # Reflexivity + axiom le(X, Y) & le(Y, Z) -> le(X, Z) # Transitivity + axiom le(X, Y) & le(Y, X) -> X = Y # Anti-symmetry + axiom le(X, Y) | le(Y, X) # Totality + + individual zero:carrier + axiom le(zero, X) + + action get_succ(x:carrier) returns (y:carrier) = { + assume le(x,y) & x ~= y & ((le(x, Z) & x ~= Z) -> le(y, Z)) + } + + action get_pred(y:carrier) returns (x:carrier) = { + assume le(x,y) & x ~= y & ((le(x, Z) & x ~= Z) -> le(y, Z)) + } +} + + +################################################################################ +# +# A module for a fifo channel +# +################################################################################ + +module fifo_channel(m_t) = { + relation le(X:m_t,Y:m_t) # partial order representing + # messages in the channel - + # larger messages are older + + conjecture le(X, Y) & le(Y, Z) -> le(X, Z) # Transitivity + conjecture le(X, Y) & le(Y, X) -> X = Y # Anti-symmetry + conjecture le(X, Y) -> le(X, X) & le(Y, Y) # Partial reflexivity + conjecture le(X, X) & le(Y, Y) -> le(X, Y) | le(Y, X) # Partial Totality + + init ~le(X, Y) + + action send(m: m_t) = { + # insert m as a newest message + assume ~le(m, m); + le(m, m) := true; + le(m, X) := le(X,X) + } + + action receive returns (m: m_t) = { + # receive the oldest message and remove it + assume le(m, m); + assume le(m,X) -> X = m; + le(X,m) := false + } + + action drop = { + # drop a message + local m: m_t { + le(X,Y) := le(X, Y) & X ~= m & Y ~= m + } + } +} + + +################################################################################ +# +# Types, relations and functions describing state of the network +# +################################################################################ + +# a totally ordered set for indices +type index +instantiate index : total_order(index) + +# an uninterpreted sort for data items +type value +individual bot:value # special bottom value + +# data messages (sent from sender to received), with a fifo channel, +# and a data item and sequence bit for every message +type data_msg_t +instantiate data_msg : fifo_channel(data_msg_t) +individual d(D:data_msg_t) : value +relation dbit(D:data_msg_t) +# need to also remember the index where the data came from +individual d_i(D:data_msg_t) : index + + + +# ack messages (sent from receiver to sender), with a fifo channel and +# a sequence number bit for every message. +type ack_msg_t +instantiate ack_msg : fifo_channel(ack_msg_t) +relation abit(A:ack_msg_t) + +# sender array and receiver array +individual sender_array(I:index) : value +individual receiver_array(I:index) : value +init receiver_array(I) = bot +init sender_array(I) ~= bot + +# sender index and receiver index +individual sender_i:index +init sender_i = index.zero +individual receiver_i:index +init receiver_i = index.zero + +# sender and receiver bits, initially 0 (false) +relation sender_bit(I:index) +init ~sender_bit(I) +relation receiver_bit(I:index) +init ~receiver_bit(I) +conjecture I ~= index.zero -> ~sender_bit(I) & ~receiver_bit(I) + +################################################################################ +# +# Protocol actions +# +################################################################################ + +action sender_send = { + # send (sender_array(sender_i), sender_bit) + local m:data_msg_t { + assume d(m) = sender_array(sender_i); + assume d_i(m) = sender_i; + assume dbit(m) <-> sender_bit(index.zero); + call data_msg.send(m) + } +} + +action sender_receive_ack = { + local a:ack_msg_t { + a := ack_msg.receive(); + if abit(a) <-> sender_bit(index.zero) { + sender_bit(index.zero) := ~sender_bit(index.zero); + sender_i := index.get_succ(sender_i); + call sender_send + } + } +} + +action receiver_receive = { + local m:data_msg_t, a:ack_msg_t { + m := data_msg.receive(); + if dbit(m) <-> receiver_bit(index.zero) { + # send ack with receiver_bit + assume abit(a) <-> receiver_bit(index.zero); + call ack_msg.send(a); + + # flip receiver bit, append to receiver array + receiver_bit(index.zero) := ~receiver_bit(index.zero); + receiver_array(receiver_i) := d(m); + receiver_i := index.get_succ(receiver_i) + } + } +} + +export sender_send +export sender_receive_ack +export receiver_receive +export data_msg.drop +export ack_msg.drop + +################################################################################ +# +# Safety and inductive invariant +# +################################################################################ + +# # Bogus conjecture used to make BMC return a trace receiver array has 4 values +# # takes around 15 seconds to find a trace +# conjecture ~( +# ~index.le(I1,index.zero) & +# ~index.le(I2, I1) & +# ~index.le(I3, I2) & +# receiver_array(I3) ~= bot +# ) + +# safety - receiver array has values from sender array +conjecture receiver_array(I) = bot | receiver_array(I) = sender_array(I) + +# conjectures obtained interactively + +conjecture sender_array(I0) ~= bot +conjecture ~(data_msg.le(D0,D0) & d(D0) ~= sender_array(I0) & sender_array(d_i(D0)) = sender_array(I0)) +conjecture ~(index.le(receiver_i,sender_i) & sender_i ~= receiver_i) + +conjecture (sender_bit(index.zero) <-> receiver_bit(index.zero)) <-> sender_i = receiver_i +conjecture index.le(I,sender_i) | index.le(receiver_i, I) diff --git a/examples/pldi16/concensus_quorum.ivy b/examples/pldi16/concensus_quorum.ivy new file mode 100644 index 000000000..b007ba44d --- /dev/null +++ b/examples/pldi16/concensus_quorum.ivy @@ -0,0 +1,116 @@ +#lang ivy1.3 + +# +# A quorum based concencus protocol. +# Similar to a single round of Paxos (I think). +# +# This has an interesting AE issue: every two quorums have a node in their intersection, +# and every decided node should have a quorum that it decided based on - this is cyclic. +# Here we get around this by remembering the quorum in the decided relation. +# + +type node +type value +type quorum + +relation member(N:node, Q:quorum) + +# forall Q1 Q2 exists N. member(N, Q1) & member(N, Q2) +individual quorum_intersection(Q1:quorum, Q2:quorum) : node # a Skolem function +axiom member(quorum_intersection(Q1, Q2), Q1) +axiom member(quorum_intersection(Q1, Q2), Q2) + +module lone(f) = { + axiom ~f(X, Y1) | ~f(X, Y2) | Y1 = Y2 +} + +relation val(N:node, V:value) # node N has value V +relation decided(N:node, Q:quorum) # node N has decided based on quorum Q + +instantiate lone(val) + +relation propose(S:node, V:value, R:node) # node S proposed value V to node R +relation ack(S:node, V:value, R:node) # node S acknowledged value V to node R +relation knowledge(X:node, Y:node, V:value) # node X knows node Y has value V + +init ~propose(X, Y, Z) +init ~ack(X, Y, Z) +init ~knowledge(X, Y, Z) +init ~decided(X, Q) +init ~val(X, Y) + + +action prop = { + local n:node, v:value { + # chose a node without a value and propose an arbitraty value to everyone (including self) + assume ~val(n, V); + propose(n, v, X) := true + } +} + +action receive_prop = { + local n1:node, n2:node, v1:value, v2:value { + # process a propose message and reply an acknowledge message + assume propose(n1, v1, n2); + if ~val(n2, V:value) & ~decided(n2, Q:quorum) { + # if we have no value and are undecided - take the proposed value + + # actually, we would like to remove the undecided part + # from the if, but this would require an AE invariant! + + val(n2, v1) := true + }; + # acknowledge back with n2's current value + assume val(n2, v2); + ack(n2, v2, n1) := true + } +} + +action receive_ack = { + local n1:node, n2:node, v:value { + # process an acknowledge message by updating the knowledge + assume ack(n1, v, n2); + knowledge(n2, n1, v) := true + } +} + +action decide = { + local n:node, v:value, q:quorum { + # assume that node n has value v, and has knowledge of a quorum that also has v, and make n decided. + assume val(n, v); + assume member(N, q) -> knowledge(n, N, v); + decided(n, q) := true + } +} + +export prop +export receive_prop +export receive_ack +export decide + + +# The safety property +conjecture (decided(N1, Q1) & decided(N2, Q2) & val(N1, V1) & val(N2, V2)) -> V1 = V2 + +# found interactiveley - second attempt (after knowing the first attempt below) +# conjecture ~(knowledge(N0,N1,V0) & ~ack(N1,V0,N0)) # taken from concensus_unanimously +# conjecture ~(ack(N1,V1,N0) & ~val(N1,V1)) # taken from concensus_unanimously +# conjecture ~(decided(N1,Q0) & member(N0,Q0) & val(N1,V1) & ~val(N0,V1)) + + +### + +# # found using IND-MUSMSS +# conjecture ~(knowledge(N1, N0, V0) & ~ack(N0, V0, N1)) +# # conjecture ~(decided(N0, Q0) & member(N0, Q0) & val(N0, V0) & ~knowledge(N0, N0, V0)) +# conjecture ~(decided(N1, Q0) & member(N0, Q0) & val(N1, V1) & ~knowledge(N1, N0, V1)) +# conjecture ~(ack(N1, V1, N0) & ~val(N1, V1)) + +### + +# found interactiveley - first attempt +# conjecture ~(knowledge(N1, N1, V0) & val(N1, V1) & V0 ~= V1) +# conjecture ~(decided(N0, Q) & member(N1, Q) & val(N0, V0) & val(N1, V1) & V0 ~= V1) +# conjecture ~(ack(N0, V1, N1) & val(N0, V0) & V1 ~= V0) +# conjecture ~(ack(N0, V0, N1) & ~val(N0, V0)) +# conjecture ~(knowledge(N0, N1, V0) & ~ack(N1, V0, N0)) diff --git a/examples/pldi16/concensus_unanimously.ivy b/examples/pldi16/concensus_unanimously.ivy new file mode 100644 index 000000000..a203ee890 --- /dev/null +++ b/examples/pldi16/concensus_unanimously.ivy @@ -0,0 +1,100 @@ +#lang ivy1.3 + +# +# A very basic exercise in verification of concencus protocols (ala Paxos). +# +# A contrived protocol that reaches concensus only when a node hears +# that all nodes have the same value. +# +# It does contain an interesting AE example (see below in the receive_prop action). +# + +type node +type value + +module lone(f) = { + axiom ~f(X, Y1) | ~f(X, Y2) | Y1 = Y2 +} + +module injective(f) = { + axiom ~f(X1, Y) | ~f(X2, Y) | X1 = X2 +} + +relation val(N:node, V:value) # node N has value V +relation decided(N:node) # node N has decided + +instantiate lone(val) + +relation propose(S:node, V:value, R:node) # node S proposed value V to node R +relation ack(S:node, V:value, R:node) # node S acknowledged value V to node R +relation knowledge(X:node, Y:node, V:value) # node X knows node Y has value V + +init ~propose(X, Y, Z) +init ~ack(X, Y, Z) +init ~knowledge(X, Y, Z) +init ~decided(X) +init ~val(X, Y) + +action prop = { + local n:node, v:value { + # chose a node without a value and propose an arbitraty value to everyone (including self) + assume ~val(n, V); + propose(n, v, X) := true + } +} + +action receive_prop = { + local n1:node, n2:node, v1:value, v2:value { + # process a propose message and reply an acknowledge message + assume propose(n1, v1, n2); + if ~val(n2, V:value) & ~decided(n2) { + # if we have no value and are undecided - take the proposed value + + # actually, we would like to remove the undecided part + # from the if, but this would require an AE invariant! + + val(n2, v1) := true + }; + # acknowledge back with n2's current value + assume val(n2, v2); + ack(n2, v2, n1) := true + } +} + +action receive_ack = { + local n1:node, n2:node, v:value { + # process an acknowledge message by updating the knowledge + assume ack(n1, v, n2); + knowledge(n2, n1, v) := true + } +} + +action decide = { + local n:node, v:value { + # assume that you know all nodes have the same value v, become decided. + assume knowledge(n, N, v); + decided(n) := true + } +} + +export prop +export receive_prop +export receive_ack +export decide + +# the safety property +conjecture (decided(N1) & decided(N2) & val(N1, V1) & val(N2, V2)) -> V1 = V2 + +# found interactiveley on first attempt +# conjecture ~(knowledge(N1, N1, V0) & val(N1, V1) & V0 ~= V1) +# conjecture ~(decided(N0) & val(N0, V1) & val(N1, V0) & V0 ~= V1) +# conjecture ~(ack(N0, V1, N1) & val(N0, V0) & V1 ~= V0) +# conjecture ~(ack(N0, V0, N0) & ~val(N0, V0)) +# conjecture ~(decided(N0) & val(N0, V1) & ~val(N1, V1)) +# conjecture ~(knowledge(N0, N1, V0) & ~ack(N1, V0, N0)) +# conjecture ~(ack(N0, V0, N1) & ~val(N0, V0)) + +# found interactively later (with knowledge of the previous invariant) +# ~(knowledge(N0,N1,V0) & ~ack(N1,V0,N0)) +# ~(ack(N0,V1,N0) & ~val(N0,V1)) # subsumed by the next one +# ~(ack(N1,V1,N0) & ~val(N1,V1)) diff --git a/examples/pldi16/ironfleet_toy_lock.ivy b/examples/pldi16/ironfleet_toy_lock.ivy new file mode 100644 index 000000000..8c31880ed --- /dev/null +++ b/examples/pldi16/ironfleet_toy_lock.ivy @@ -0,0 +1,112 @@ +#lang ivy1.3 + +# +# An Ivy model of the toy lock example from https://github.com/Microsoft/Ironclad/blob/master/ironfleet/src/Dafny/Distributed/Protocol/Lock/Node.i.dfy +# + +# A total order helper module +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 state of the network +# +################################################################################ + +type node +type epoch + +# epochs are totally ordered with a least element called zero +relation le(X:epoch, Y:epoch) +instantiate total_order(le) +individual zero:epoch +axiom le(zero, X) + +individual ep(N:node) : epoch # ep(n) is the current epoch of node n + +relation held(N:node) # held(n) is true iff the lock is currently held by node n + +# initially exactly one node holds the lock, and all others have epoch zero +individual first:node +init held(X) <-> X=first +init N ~= first -> ep(N) = zero + +# transfer messages +relation transfer(E:epoch, N:node) # the node is the message destination +init ~transfer(E, N) + +# locked messages +relation locked(E:epoch, N:node) # the node is the message source +init ~locked(E, N) + +################################################################################ +# +# Protocol description +# +################################################################################ + +action grant = { + local n1:node, n2:node, e:epoch { + # release the lock and send a transfer message + assume held(n1); + assume ~le(e, ep(n1)); # jump to some strictly higher epoch + transfer(e, n2) := true; + held(n1) := false + } +} + +action accept = { + local n:node, e:epoch { + # receive a transfer message and take the lock, sending a locked message + assume transfer(e,n); + if ~le(e, ep(n)) { + held(n) := true; + ep(n) := e; + locked(e, n) := true + } + } +} + +export grant +export accept + +# a bogous conjecture to use BMC to test aht we can actually transfer the lock +# conjecture locked(E, N) -> N = first + +# the safety property +conjecture locked(E, N1) & locked(E, N2) -> N1 = N2 + +# obtained interactively from CTI's (first attempt) +# conjecture ~(locked(E1,N0) & transfer(E1,N1) & N1 ~= N0) # not really needed +# conjecture ~(le(ep(N1),E1) & locked(E1,N1) & E1 ~= ep(N1)) +# conjecture ~(held(N1) & le(ep(N1),E1) & locked(E1,N0) & N1 ~= N0) # not really needed +# conjecture ~(transfer(E1,N0) & transfer(E1,N1) & N1 ~= N0) +# conjecture ~(held(N1) & le(ep(N1),E1) & transfer(E1,N1) & E1 ~= ep(N1)) # not really needed +# conjecture ~(held(N0) & le(ep(N0),E1) & transfer(E1,N1) & E1 ~= ep(N0)) +# conjecture ~(held(N0) & held(N1) & N1 ~= N0) # not really needed +# conjecture ~(le(ep(N0),E1) & le(ep(N0),E2) & transfer(E1,N0) & transfer(E2,N0) & E2 ~= E1 & ep(N0) ~= E1 & ep(N0) ~= E2) # not really needed +# conjecture ~(transfer(ep(N1),N0) & N1 ~= N0) # not really needed +# conjecture ~(held(N1) & le(ep(N1),ep(N0)) & N1 ~= N0) +# conjecture ~(le(E1,ep(N1)) & le(ep(N0),E1) & transfer(E1,N0) & ep(N0) ~= E1) +# conjecture ~(le(E1,E2) & le(ep(N0),E1) & transfer(E1,N0) & transfer(E2,N1) & E2 ~= E1 & ep(N0) ~= E1) + +# the invariant of the first attempt after removal of unnecessary conjectures: +# conjecture ~(le(ep(N1),E1) & locked(E1,N1) & E1 ~= ep(N1)) +# conjecture ~(transfer(E1,N0) & transfer(E1,N1) & N1 ~= N0) +# conjecture ~(held(N0) & le(ep(N0),E1) & transfer(E1,N1) & E1 ~= ep(N0)) +# conjecture ~(held(N1) & le(ep(N1),ep(N0)) & N1 ~= N0) +# conjecture ~(le(E1,ep(N1)) & le(ep(N0),E1) & transfer(E1,N0) & ep(N0) ~= E1) +# conjecture ~(le(E1,E2) & le(ep(N0),E1) & transfer(E1,N0) & transfer(E2,N1) & E2 ~= E1 & ep(N0) ~= E1) + +# a prettyfied version of the above invariant +conjecture transfer(E, N1) & transfer(E, N2) -> N1 = N2 # epochs transfer to at most one node +conjecture locked(E, N) -> le(E, ep(N)) # if a node sent a locked msg, the node's epoch is now higher +conjecture held(N) & N ~= M -> ~le(ep(N), ep(M)) # holding node's epoch is higher than any other node's epoch (this implies a single node holds the lock) +conjecture held(N) & transfer(E, M) -> le(E, ep(N)) # holding node's epoch is higher than any transfer's epoch +conjecture transfer(E, N) & ~le(E, ep(N)) -> ~le(E, ep(M)) # pending transfer epoch is higher than any node's epoch +conjecture transfer(E, N) & ~le(E, ep(N)) & transfer(F, M) -> le(F, E) # pending transfer epoch is higher than any transfer's epoch diff --git a/examples/pldi16/leader_election_ring_btw_nonreflexive.ivy b/examples/pldi16/leader_election_ring_btw_nonreflexive.ivy new file mode 100644 index 000000000..ca4dcfb77 --- /dev/null +++ b/examples/pldi16/leader_election_ring_btw_nonreflexive.ivy @@ -0,0 +1,129 @@ +#lang ivy1.3 + +################################################################################ +# +# A 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 +} + + +################################################################################ +# +# Module describing a ring topology. +# +# The module includes an anti-reflexive ternary btw relation. +# +# The module also includes get_next and get_prev actions. +# +# In this module, the ring topology is arbitrary and fixed. +# +################################################################################ + +module ring_topology(carrier) = { + + relation btw(X:carrier,Y:carrier, Z:carrier) # Y is on the acyclic path from X to Z + + # Axiom defining the btw relation - note it's not reflexive + # not needed: axiom btw(X,Y,Z) -> X ~= Y & X ~= Z & Y ~= Z # anti-reflexive + axiom btw(W,X,Y) & btw(W,Y,Z) -> btw(W,X,Z) # transitive + axiom btw(W,X,Y) -> ~btw(W,Y,X) # acyclic + axiom btw(W,X,Y) | btw(W,Y,X) | W=X | W=Y | X=Y # total + axiom btw(X,Y,Z) -> btw(Y,Z,X) # cyclic permutations + + action get_next(x:carrier) returns (y:carrier) = { + assume x ~= y & ((Z ~= x & Z ~= y) -> btw(x,y,Z)) + } + + action get_prev(y:carrier) returns (x:carrier) = { + assume y ~= x & ((Z ~= y & Z ~= x) -> btw(y,x,Z)) + } + +} + + +################################################################################ +# +# Types, relations and functions describing state of the network +# +################################################################################ + +type node +type id + +# A ring topology of nodes +instantiate ring : ring_topology(node) + +# A total order on ids +relation le(X:id, Y:id) +instantiate total_order(le) + +# A function relating a node to its id +individual idn(X:node) : id +axiom idn(X) = idn(Y) -> X = Y # the idn function is injective + +# A relation that keeps track of nodes that think they are the leader +relation leader(N:node) +init ~leader(N) + +# A relation for pending messages, a message is just an id +relation pending(V:id, N:node) # The identity V is pending at node N +init ~pending(V, N) + + +################################################################################ +# +# Protocol description +# +# Two action: send and receive +# +################################################################################ + +action send = { + local n1:node, n2:node { + # send my own id to the next node + n2 := ring.get_next(n1); + pending(idn(n1), n2) := true + } +} + +action receive = { + local n1:node, n2:node, m:id { + # receive a message from the right neighbor + assume pending(m, n1); + pending(m, n1) := *; # abstract the number of pending messages + if m = idn(n1) { # Found a leader + leader(n1) := true + } else { + if le(idn(n1), m) { # pass message to next node + n2 := ring.get_next(n1); + pending(m, n2) := true + } # otherwise drop the message... + } + } +} + +export send +export receive + +# bogus conjecture +# conjecture ~( +# N1 ~= N2 & +# N1 ~= N3 & +# N2 ~= N3 & +# leader(N1) +# ) + +# The safety property: +conjecture leader(X) & leader(Y) -> X = Y # at most one leader + +# conjectures obtained via CTI's +# conjecture ~(le(idn(N1),idn(N0)) & pending(idn(N1),N1) & idn(N1) ~= idn(N0)) +# conjecture ~(le(idn(N2),idn(N0)) & pending(idn(N2),N1) & ring.btw(N0,N1,N2)) +# conjecture ~(le(idn(N1),idn(N0)) & leader(N1) & N1 ~= N0) diff --git a/examples/pldi16/learning_switch_nodom.ivy b/examples/pldi16/learning_switch_nodom.ivy new file mode 100644 index 000000000..f7a2d8afe --- /dev/null +++ b/examples/pldi16/learning_switch_nodom.ivy @@ -0,0 +1,118 @@ +#lang ivy1.3 + +################################################################################ +# +# Module describing an acyclic partial function. The function is built by +# calling the "set" action. This has preconditions that enforce the required +# invariants. The function can be accessed using "dom" to query if an element is +# in the domain of the function, and "get" to get its value. The "get" action +# has a precondition that the given element must be in the domain. +# +# Because of the invariant that the relation re construct by "set" is an acyclic +# partial function, we can represent it by its transitive closure "tc", while +# remainin in EPR. +# +################################################################################ + +module acyclic_partial_function(carrier) = { + relation tc(X:carrier,Y:carrier) # transitive closure of the function + + # Conjectures that ensure that tc really describes the transitive closure + # of an acyclic partial function. + # These conjectures form part of the safety property. + conjecture tc(X,X) # Reflexivity + conjecture tc(X, Y) & tc(Y, Z) -> tc(X, Z) # Transitivity + conjecture tc(X, Y) & tc(Y, X) -> X = Y # Anti-symmetry + conjecture tc(X, Y) & tc(X, Z) -> (tc(Y, Z) | tc(Z, Y)) # Semi-linearity + + init (tc(X,Y) <-> X = Y) #initially empty + + + action set(x:carrier,y:carrier) = { + tc(X, Y) := tc(X, Y) | (tc(X, x) & tc(y, Y)) + } + + action get(x:carrier) returns (y:carrier) = { + assume tc(x,y) & x ~= y & ((tc(x, Z) & x ~= Z) -> tc(y, Z)) + } +} + +################################################################################ +# +# Types, relations and functions describing state of the network +# +################################################################################ + +type packet +type node + +relation pending(P:packet, S:node, T:node) # relation for pending packets +individual src(P:packet) : node # function src : packet -> node +individual dst(P:packet) : node # function dst : packet -> node +relation link(S:node, T:node) # relation for network topology +instantiate route(N:node) : acyclic_partial_function(node) # routing tables + +axiom ~link(X, X) # no self-loops in links +axiom ~link(X, Y) | link(Y, X) # symmetric links + +# The initial state of the network (empty) + +init ~pending(P,S,T) + +################################################################################ +# +# Protocol description +# +# Two action: new_packet and receive +# +################################################################################ + +action new_packet = { + local p:packet { + # Create a new packet, by adding it to pending from the src to itself + pending(p, src(p), src(p)) := true + } +} + +action receive = { + local p:packet, sw0:node, sw1:node, sw2:node { + # receive a pending packet from sw0 to sw1 and process it + + ######################################## + # The action's guard. + assume pending(p, sw0, sw1); + + ######################################## + # Abstract the number of times that the same packet recieved + pending(p, sw0, sw1) := *; + + ######################################## + # learn: if no route from receiving switch back to source... + if ((route(src(p)).tc(sw1,X:node) -> X:node=sw1) & src(p) ~= sw1) { + call route(src(p)).set(sw1, sw0) # create new route from sw1 to sw0 + }; + + ######################################## + # forward the packet if destination is not self + if dst(p) ~= sw1 { + if (route(dst(p)).tc(sw1,X:node) -> X:node=sw1) { # if no route from sw1 to to dst(p)... + pending(p, sw1, Y) := link(sw1, Y) & Y ~= sw0 # flood + } else { + sw2 := route(dst(p)).get(sw1); # get the routing table entry + pending(p, sw1, sw2) := true # route the packet there + } + } + } +} + +export new_packet +export receive + +# The safety property is given by the conjectures of the +# acyclic_partial_function module, that state that the routing tables +# do not create cycles. + +# obtained interactively via CTI's +conjecture ~(route.tc(N1,N1,N0) & N1 ~= N0) +conjecture ~(route.tc(N2,N1,N0) & ~route.tc(N2,N1,N2) & N1 ~= N0) +conjecture ~(pending(P0,N2,N1) & ~route.tc(src(P0),N2,src(P0))) diff --git a/examples/pldi16/verdi_mutex.ivy b/examples/pldi16/verdi_mutex.ivy new file mode 100644 index 000000000..19756e99a --- /dev/null +++ b/examples/pldi16/verdi_mutex.ivy @@ -0,0 +1,219 @@ +#lang ivy1.3 + +# +# The Mutex example (Figure 3) from the Verdi paper's overview section. +# +# This file also includes two modules used to model lists and message +# pools. +# +# [Verdi] Wilcox, James R., et al. "Verdi: A framework for +# implementing and formally verifying distributed systems." PLDI 2015. +# +# + + + +################################################################################ +# +# Module describing an ordered list. The list may contain multiple +# occurences of the same data element. The list contains derived +# relations to test if it's empty, and to test if a data element is at +# the head of the list. +# +################################################################################ + +type list_elem # used to allow multiple identical messages and list items + +module list(data_t) = { + individual data(U:list_elem) : data_t # function from elements to data + individual h : list_elem + relation le(X:list_elem,Y:list_elem) # the list order on elements + relation empty # should be a function when langauge enables it + relation at_head(D:data_t) # true only for the data at the head of the list, empty if the list is empty + + # Conjectures that ensure that le is a total linear order over its support + conjecture le(X,Y) -> (le(X,X) & le(Y,Y)) # Reflexivity + conjecture le(X,Y) & le(Y,Z) -> le(X,Z) # Transitivity + conjecture le(X,Y) & le(Y,X) -> X = Y # Anti-symmetry + conjecture le(X,X) & le(Y,Y) -> (le(X,Y) | le(Y,X)) # Linearity + + # empty, h, and at_head + conjecture empty -> ~le(X,Y) + conjecture ~empty -> le(h, h) + conjecture le(X, X) -> le(h, X) + conjecture at_head(D) -> le(h, h) & data(h) = D + conjecture le(h, h) -> at_head(data(h)) + + init empty + init ~le(X,Y) + init ~at_head(D) + + action append(x:data_t) = { + local u:list_elem { + assume ~le(u, X) & ~le(X, u); + data(u) := x; + le(u, u) := true; + le(X, Y) := le(X, Y) | (le(X, X) & Y = u); + if empty { + h := u + }; + empty := false; + at_head(D) := D = data(h) + } + } + + action pop returns (x:data_t) = { + local u:list_elem { + assume le(u, u) & (le(X,X) -> le(u, X)); + x := data(u); + le(X, Y) := le(X, Y) & (X ~= u); + h := *; + assume le(X, X) -> le(h, X); + if ~le(X:list_elem,X:list_elem) { + empty := true; + at_head(D) := false + } else { + at_head(D) := D = data(h) + } + } + } + + action get_head returns (x:data_t) = { + assume at_head(x) + } +} + +################################################################################ +# +# Module describing a message pool with one message field. +# +# Messages can be sent and received, and multiple messages with the +# same field are supported. +# +################################################################################ + + +module msg_pool(msg_t, field_t) = { + relation pending(M:msg_t) + individual fld(M:msg_t) : field_t + + init ~pending(M) + + action send(f:field_t) = { + local m:msg_t { + assume ~pending(m); + fld(m) := f; + pending(m) := true + } + } + + action receive returns (f:field_t) = { + local m:msg_t { + assume pending(m); + f := fld(m); + pending(m) := false + } + } +} + +################################################################################ +# +# Types, relations and functions describing state of the network +# +################################################################################ + +type client +type lock_m +type unlock_m +type grant_m + +relation has_lock(C:client) +instantiate lock_msg : msg_pool(lock_m, client) +instantiate unlock_msg : msg_pool(unlock_m, client) +instantiate grant_msg : msg_pool(grant_m, client) +instantiate waiting : list(client) # list of waiting clients + +init ~has_lock(C) + +################################################################################ +# +# Protocol description +# +################################################################################ + +action send_lock = { + local c:client { + # A lock event - client requests lock + call lock_msg.send(c) + } +} + +action send_unlock = { + local c:client { + # An unlock event - client requests unlock + assume has_lock(c); + has_lock(c) := false; + call unlock_msg.send(c) + } +} + +action receive_lock = { + local c:client { + c := lock_msg.receive; + if waiting.empty { + call grant_msg.send(c) + }; + call waiting.append(c) + } +} + +action receive_unlock = { + local c:client, ignore:client { + ignore := unlock_msg.receive; + ignore := waiting.pop; + if ~waiting.empty { + c := waiting.get_head; + call grant_msg.send(c) + } + } +} + +action receive_grant = { + local c:client { + c := grant_msg.receive; + has_lock(c) := true + } +} + +export send_lock +export send_unlock +export receive_lock +export receive_unlock +export receive_grant + +# just a bogus conjecture used with BMC to make sure we CAN have a client that holds the lock +#conjecture ~has_lock(C1) + +# The safety property is that no two different clients have the lock +conjecture has_lock(C1) & has_lock(C2) -> C1 = C2 + +# obtained interactively via CTI's (took less than an hour) +# conjecture ~(grant_msg.pending(G0) & ~waiting.at_head(grant_msg.fld(G0))) +# conjecture ~(grant_msg.pending(G0) & unlock_msg.pending(U0)) +# conjecture ~(has_lock(C0) & ~waiting.at_head(C0)) +# conjecture ~(has_lock(C0) & unlock_msg.pending(U0)) +# conjecture ~(grant_msg.pending(G0) & has_lock(C0)) +# conjecture ~(unlock_msg.pending(U0) & ~waiting.at_head(unlock_msg.fld(U0))) +# conjecture ~(grant_msg.pending(G0) & grant_msg.pending(G1) & G1 ~= G0) +# conjecture ~(unlock_msg.pending(U0) & unlock_msg.pending(U1) & U1 ~= U0) + +# obtained interactively via CTI's at the Skype demo with the Verdi team, took about an hour +# (minimization of has_lock lock_msg.pending unlock_msg.pending grant_msg.pending waiting.le) +# ~(has_lock(C0) & ~waiting.at_head(C0)) +# ~(grant_msg.pending(G0) & ~waiting.at_head(grant_msg.fld(G0))) +# ~(grant_msg.pending(G0) & unlock_msg.pending(U0)) +# ~(grant_msg.pending(G0) & has_lock(C0)) +# ~(unlock_msg.pending(U0) & ~waiting.at_head(unlock_msg.fld(U0))) +# ~(has_lock(C0) & unlock_msg.pending(U0)) +# ~(unlock_msg.pending(U0) & unlock_msg.pending(U1) & U1 ~= U0) +# ~(grant_msg.pending(G0) & grant_msg.pending(G1) & G1 ~= G0) diff --git a/ivy/ivy_actions.py b/ivy/ivy_actions.py index 39968353e..e7886a975 100644 --- a/ivy/ivy_actions.py +++ b/ivy/ivy_actions.py @@ -1334,7 +1334,7 @@ def recur(action,annot,env,pos=None): recur(action.failed_action(),annot,env) return handler.handle(action,env) - iu.dbg('action') - iu.dbg('annot') + # iu.dbg('action') + # iu.dbg('annot') recur(action,annot,dict()) diff --git a/ivy/ivy_check.py b/ivy/ivy_check.py index 55a492fb5..b9553dce7 100644 --- a/ivy/ivy_check.py +++ b/ivy/ivy_check.py @@ -18,6 +18,7 @@ import ivy_theory as ith import ivy_transrel as itr import ivy_solver as islv +from ivy_l2s import l2s import sys from collections import defaultdict @@ -36,7 +37,7 @@ def display_cex(msg,ag): ui.ui_main_loop(ag) exit(1) raise iu.IvyError(None,msg) - + def check_properties(): if itp.false_properties(): if diagnose.get(): @@ -68,7 +69,7 @@ def show_counterexample(ag,state,bmc_res): gui.tk.mainloop() exit(1) - + def check_conjectures(kind,msg,ag,state): failed = itp.undecided_conjectures(state) if failed: @@ -87,13 +88,12 @@ def check_conjectures(kind,msg,ag,state): def has_temporal_stuff(f): return any(True for x in lut.temporals_ast(f)) or any(True for x in lut.named_binders_ast(f)) - + def check_temporals(): props = im.module.labeled_props proved = [] for prop in props: if prop.temporal: - from ivy_l2s import l2s mod = im.module.copy() mod.labeled_axioms.extend(proved) mod.labeled_props = [] @@ -139,7 +139,7 @@ def get_checked_actions(): def print_dots(): print '...', sys.stdout.flush() - + class Checker(object): def __init__(self,conj,report_pass=True): @@ -171,7 +171,7 @@ def pretty_lineno(ast): def pretty_lf(lf,indent=8): return indent*' ' + "{}{}".format(pretty_lineno(lf),pretty_label(lf.label)) - + class ConjChecker(Checker): def __init__(self,lf,indent=8): self.lf = lf @@ -180,7 +180,7 @@ def __init__(self,lf,indent=8): def start(self): print pretty_lf(self.lf,self.indent), print_dots() - + class ConjAssumer(Checker): def __init__(self,lf): self.lf = lf @@ -234,7 +234,7 @@ def show_sym(self,sym,renamed_sym): continue self.current[lhs] = rhs print ' {}'.format(rfmla) - + def eval(self,cond): truth = self.model.eval_to_constant(cond) if lg.is_false(truth): @@ -242,9 +242,9 @@ def eval(self,cond): elif lg.is_true(truth): return True assert False,truth - + def handle(self,action,env): - + # iu.dbg('env') if hasattr(action,'lineno'): # print ' env: {}'.format('{'+','.join('{}:{}'.format(x,y) for x,y in env.iteritems())+'}') @@ -264,7 +264,7 @@ def end(self): for sym in self.vocab: if not itr.is_new(sym) and not itr.is_skolem(sym): self.show_sym(sym,sym) - + def filter_fcs(fcs): @@ -426,7 +426,7 @@ def summarize_isolate(mod): check_conjs_in_state(mod,ag,post,indent=12) else: print '' - + callgraph = defaultdict(list) @@ -501,7 +501,6 @@ def check_isolate(): if temporals: if len(temporals) > 1: raise IvyError(None,'multiple temporal properties in an isolate not supported yet') - from ivy_l2s import l2s l2s(mod, temporals[0]) mod.concept_spaces = [] mod.update_conjs() @@ -565,7 +564,7 @@ def check_module(): else: if coverage.get(): missing = ivy_isolate.check_isolate_completeness() - + if missing: raise iu.IvyError(None,"Some assertions are not checked") @@ -608,4 +607,3 @@ def main(): if __name__ == "__main__": main() - diff --git a/ivy/ivy_compiler.py b/ivy/ivy_compiler.py index a689a94fb..cfb018b2e 100644 --- a/ivy/ivy_compiler.py +++ b/ivy/ivy_compiler.py @@ -1310,10 +1310,6 @@ def named_trans(prop): mod.labeled_props.append(g.clone([label,g.formula])) mod.labeled_props.append(prop) mod.subgoals.append((prop,subgoals)) - # elif prop.temporal: - # from ivy_l2s import l2s - # print "=================" + "\n" * 10 - # l2s(mod, prop) else: mod.labeled_props.append(prop) if prop.id in nmap: diff --git a/ivy/ivy_graph.py b/ivy/ivy_graph.py index 356632727..29938982b 100644 --- a/ivy/ivy_graph.py +++ b/ivy/ivy_graph.py @@ -709,7 +709,7 @@ def materialize(self,node,recomp=False): return witness_concept(witness) def empty_edge(self,edge,recomp=False): - self.materialize_edge(edge,false) + self.materialize_edge(edge,False) def materialize_edge(self,edge,truth,recomp=False): rel,head,tail = edge diff --git a/ivy/ivy_l2s.py b/ivy/ivy_l2s.py index 8ad70a392..4e08587ab 100644 --- a/ivy/ivy_l2s.py +++ b/ivy/ivy_l2s.py @@ -8,29 +8,36 @@ TODO's and open issues: -* automatically add conjectures of original system to the saved state +* allow exporting and using of temporal properties + +* support for ivy1.7 syntax -* automatically add basic conjectures about the monitor (e.g. states - are mutually exclusive) +* add support for enumerated types + +* add support for adding all elements smaller than a constant (downward finite total order) + +* automatically add conjectures of original system to the saved state * handle multiple temporal properties * temporal axioms? -* support nesting structure? - * review the correctness -* figure out the public_actions issue - * decide abotu normalizing the Boolean structure of temporal formulas, properties, waited formulas, and named binders (e.g. normalize ~~phi to phi?) -* a syntax for accessing Skolem constants and functions from the +* syntax for accessing Skolem constants and functions from the negation of temporal properties. +* syntax for fair scheduling of actions (e.g., eliminate scheduled + from ticket) +* use assetions instead of l2s_error +""" + +""" Useful definitions from ivy_module: self.definitions = [] # TODO: these are actually "derived" relations self.labeled_axioms = [] @@ -50,18 +57,20 @@ from ivy_actions import (AssignAction, Sequence, ChoiceAction, AssumeAction, AssertAction, HavocAction, concat_actions) +import ivy_ast as ast import logic as lg import ivy_logic_utils as ilu import ivy_utils as iu + debug = iu.BooleanParameter("l2s_debug",False) + def forall(vs, body): return lg.ForAll(vs, body) if len(vs) > 0 else body -def l2s(mod, lf): - +def l2s(mod, temporal_goal): # modify mod in place # module pass helper funciton @@ -80,6 +89,7 @@ def mod_pass(transform): l2s_waiting = lg.Const('l2s_waiting', lg.Boolean) l2s_frozen = lg.Const('l2s_frozen', lg.Boolean) l2s_saved = lg.Const('l2s_saved', lg.Boolean) + l2s_error = lg.Const('l2s_error', lg.Boolean) l2s_d = lambda sort: lg.Const('l2s_d',lg.FunctionSort(sort,lg.Boolean)) l2s_a = lambda sort: lg.Const('l2s_a',lg.FunctionSort(sort,lg.Boolean)) l2s_w = lambda vs, t: lg.NamedBinder('l2s_w', vs, t) @@ -87,6 +97,24 @@ def mod_pass(transform): l2s_g = lambda vs, t: lg.NamedBinder('l2s_g', vs, t) old_l2s_g = lambda vs, t: lg.NamedBinder('old_l2s_g', vs, t) + # add conjectures about monitor state + conjs = [ + lg.Or(l2s_waiting, l2s_frozen, l2s_saved), + lg.Or(lg.Not(l2s_waiting), lg.Not(l2s_frozen)), + lg.Or(lg.Not(l2s_waiting), lg.Not(l2s_saved)), + lg.Or(lg.Not(l2s_frozen), lg.Not(l2s_saved)), + ] + for f in conjs: + c = ast.LabeledFormula(ast.Atom('l2s_internal'), f) + c.lineno = temporal_goal.lineno + mod.labeled_conjs.append(c) + + # add conjecture that we are not in the error state (this is + # instead of using an assertion. see below) + c = ast.LabeledFormula(ast.Atom('not_l2s_error'), lg.Not(l2s_error)) + c.lineno = temporal_goal.lineno + mod.labeled_conjs.append(c) + #print ilu.used_symbols_asts(mod.labeled_conjs) #print '='*40 #print list(ilu.named_binders_asts(mod.labeled_conjs)) @@ -105,7 +133,7 @@ def _l2s_g(vs, t): return res replace_temporals_by_l2s_g = lambda ast: ilu.replace_temporals_by_named_binder_g_ast(ast, _l2s_g) mod_pass(replace_temporals_by_l2s_g) - not_lf = replace_temporals_by_l2s_g(lg.Not(lf.formula)) + not_temporal_goal = replace_temporals_by_l2s_g(lg.Not(temporal_goal.formula)) if debug.get(): print "=" * 80 +"\nafter replace_temporals_by_named_binder_g_ast"+ "\n"*3 print "=" * 80 + "\nl2s_gs:" @@ -122,7 +150,9 @@ def _l2s_g(vs, t): print_module(mod) print "=" * 80 + "\n"*3 - # TODO: what about normalizing lf? + # TODO: what about normalizing temporal_goal? - temporal_goal + # should not contain any named binders except for temporal + # properties, so it is normalized by construction # construct the monitor related building blocks @@ -144,7 +174,7 @@ def _l2s_g(vs, t): named_binders_conjs = defaultdict(list) # dict mapping names to lists of (vars, body) for b in ilu.named_binders_asts(mod.labeled_conjs): named_binders_conjs[b.name].append((b.variables, b.body)) - named_binders_conjs = defaultdict(list,((k,list(set(v))) for k,v in named_binders_conjs.iteritems())) + named_binders_conjs = defaultdict(list,((k,sorted(list(set(v)))) for k,v in named_binders_conjs.iteritems())) to_wait = [] # list of (variables, term) corresponding to l2s_w in conjectures to_wait += named_binders_conjs['l2s_w'] to_save = [] # list of (variables, term) corresponding to l2s_s in conjectures @@ -154,8 +184,8 @@ def _l2s_g(vs, t): print "=" * 40 + "\nto_wait:\n" for vs, t in to_wait: print vs, t - print list(ilu.variables_ast(t)) == list(vs) - print + # print list(ilu.variables_ast(t)) == list(vs) + # print print "=" * 40 save_state = [ @@ -176,8 +206,9 @@ def _l2s_g(vs, t): update_w = [ AssignAction( l2s_w(vs,t)(*vs), - lg.And(l2s_w(vs,t)(*vs), lg.Not(t), replace_temporals_by_l2s_g(lg.Not(lg.Globally(lg.Not(t))))) - # TODO check this and make sure its correct + lg.And(l2s_w(vs,t)(*vs), lg.Not(t), replace_temporals_by_l2s_g(lg.Not(lg.Globally(ilu.negate(t))))) + # ($l2s_w. phi) waits until ( phi | globally ~phi), but + # ($l2s_w. ~phi) waits until (~phi | globally phi) (i.e., we avoid "globally ~~phi" here) # note this adds to l2s_gs ) for vs, t in to_wait @@ -219,8 +250,21 @@ def _l2s_g(vs, t): isinstance(t.sort, lg.FunctionSort) and isinstance(t.sort.range, lg.UninterpretedSort) ) ] - assert_no_fair_cycle = AssertAction(lg.Not(lg.And(*fair_cycle))) - assert_no_fair_cycle.lineno = lf.lineno + if debug.get(): + print "=" * 40 + "\nfair_cycle:\n" + for x in fair_cycle: + print x + print + print "=" * 40 + # TODO: figure out why AssertAction doesn't work properly + def assert_no_fair_cycle(a): + # comment and uncomment the following lines to debug: + # res = AssertAction(lg.Not(lg.And(*fair_cycle))) + # res = AssertAction(lg.false) + # res.lineno = temporal_goal.lineno + # res.lineno = a.lineno + res = AssignAction(l2s_error, lg.And(*fair_cycle)) + return res monitor_edge = lambda s1, s2: [ AssumeAction(s1), @@ -234,55 +278,24 @@ def _l2s_g(vs, t): [AssumeAction(x) for x in done_waiting] + reset_a )), - # # frozen -> saved - # Sequence(*( - # monitor_edge(l2s_frozen, l2s_saved) + - # save_state + - # reset_w - # )), + # frozen -> saved + Sequence(*( + monitor_edge(l2s_frozen, l2s_saved) + + save_state + + reset_w + )), # stay in same state (self edge) Sequence(), )] - # tableau construction (sort of) - - # Note that we first transformed globally and eventually to named - # binders, in order to normalize. Without this, we would get - # multiple redundant axioms like: - # forall X. (globally phi(X)) -> phi(X) - # forall Y. (globally phi(Y)) -> phi(Y) - # and the same redundancy will happen for transition updates. - - # temporals = [] - # temporals += list(ilu.temporals_asts( - # # TODO: these should be handled by mod_pass instead (and come via l2s_gs): - # # mod.labeled_axioms + - # # mod.labeled_props + - # [lf] - # )) - # temporals += [lg.Globally(lg.Not(t)) for vs, t in to_wait] - # temporals += [lg.Globally(t) for vs, t in l2s_gs] - # # TODO get from temporal axioms and temporal properties as well - # print '='*40 + "\ntemporals:" - # for t in temporals: - # print t, '\n' - # print '='*40 - # to_g = [ # list of (variables, formula) - # (tuple(sorted(ilu.variables_ast(tt))), tt) # TODO what about variable normalization?? - # for t in temporals - # for tt in [t.body if type(t) is lg.Globally else - # lg.Not(t.body) if type(t) is lg.Eventually else 1/0] - # ] - # TODO: get rid of the above, after properly combining it + # tableau construction to_g = [] # list of (variables, formula) - to_g += list(l2s_gs) - to_g = list(set(to_g)) + to_g += sorted(list(l2s_gs)) if debug.get(): print '='*40 + "\nto_g:\n" - for vs, t in sorted(to_g): + for vs, t in to_g: print vs, t, '\n' print '='*40 - assume_g_axioms = [ AssumeAction(forall(vs, lg.Implies(l2s_g(vs, t)(*vs), t))) for vs, t in to_g @@ -295,14 +308,8 @@ def _l2s_g(vs, t): # now patch the module actions with monitor and tableau - if debug.get(): print "public_actions:", mod.public_actions - # TODO: this includes the succ action (for the ticket example of - # test/test_liveness.ivy). seems to be a bug, and this causes - # wrong behavior for the monitor, since a call to succ from within - # another action lets it take a step - for a in mod.public_actions: action = mod.actions[a] add_params_to_d = [ @@ -310,6 +317,8 @@ def _l2s_g(vs, t): for p in action.formal_params ] new_action = concat_actions(*( + # TODO: check this with Sharon + assume_g_axioms + change_monitor_state + add_params_to_d + update_g + @@ -317,7 +326,7 @@ def _l2s_g(vs, t): assume_g_axioms + add_consts_to_d + update_w + - [assert_no_fair_cycle] + [assert_no_fair_cycle(action)] )) new_action.lineno = action.lineno new_action.formal_params = action.formal_params @@ -328,11 +337,12 @@ def _l2s_g(vs, t): AssignAction(l2s_waiting, lg.true), AssignAction(l2s_frozen, lg.false), AssignAction(l2s_saved, lg.false), + AssignAction(l2s_error, lg.false), ] l2s_init += add_consts_to_d l2s_init += reset_w l2s_init += assume_g_axioms - l2s_init += [AssumeAction(not_lf)] + l2s_init += [AssumeAction(not_temporal_goal)] mod.initializers.append(('l2s_init', Sequence(*l2s_init))) if debug.get(): @@ -349,8 +359,16 @@ def _l2s_g(vs, t): (y for x,y in mod.initializers), )): named_binders[b.name].append(b) - named_binders = defaultdict(list, ((k,list(sorted(set(v)))) for k,v in named_binders.iteritems())) - # make sure old_l2s_g is consistent with l2s_g + # sort named binders according to a consistent order + named_binders = defaultdict(list, ( + (k,list(sorted( + set(v), + key=lambda x: (len(x.variables), str(x.variables), str(x.body)), + ))) + for k,v in named_binders.iteritems() + )) + # make sure old_l2s_g is consistent with l2s_g, so that + # old_l2s_g_X is really old l2s_g_X after the substitution assert len(named_binders['l2s_g']) == len(named_binders['old_l2s_g']) assert named_binders['old_l2s_g'] == [ lg.NamedBinder('old_l2s_g', b.variables, b.body) @@ -363,8 +381,10 @@ def _l2s_g(vs, t): ) if debug.get(): print "=" * 80 + "\nsubs:" + "\n"*3 - for k, v in subs.items(): - print k, ' : ', v, '\n' + for k in sorted(named_binders.keys()): + v = named_binders[k] + for i, b in enumerate(v): + print '{}_{}'.format(k, i), ' : ', b print "=" * 80 + "\n"*3 mod_pass(lambda ast: ilu.replace_named_binders_ast(ast, subs)) diff --git a/ivy/ivy_logic_utils.py b/ivy/ivy_logic_utils.py index 1db62e690..cf2278462 100644 --- a/ivy/ivy_logic_utils.py +++ b/ivy/ivy_logic_utils.py @@ -203,12 +203,16 @@ def normalize_free_variables(ast): subs = dict() vs = [] nvs = [] + seen = set() for v in variables_ast(ast): - if v not in subs: + if v not in seen: + seen.add(v) + assert v.name not in subs # we have a problem if two different variables have the same name nv = lg.Var('V{}'.format(len(subs)), v.sort) subs[v.name] = nv vs.append(v) nvs.append(nv) + assert len(set(nvs)) == len(nvs) nast = substitute_ast(ast, subs) return vs, nvs, nast diff --git a/ivy/ivy_solver.py b/ivy/ivy_solver.py index e32a10a7b..e45291c98 100644 --- a/ivy/ivy_solver.py +++ b/ivy/ivy_solver.py @@ -10,6 +10,7 @@ from collections import defaultdict import re import functools +import random import z3 import ivy_logic @@ -32,15 +33,16 @@ use_z3_enums = False def set_seed(seed): - print 'setting seed to {}'.format(seed) + print 'setting smt seed to {}'.format(seed) z3.set_param('smt.random_seed',seed) + # TODO: should we also set sat.random_seed? -opt_seed = iu.Parameter("seed",0,process=int) +opt_seed = iu.Parameter("seed",0,process=lambda seed: random.randint(0,4294967295) if seed in ('r', 'rand', 'random') else int(seed)) opt_seed.set_callback(set_seed) def set_macro_finder(truth): z3.set_param('smt.macro_finder',truth) - + opt_incremental = iu.BooleanParameter("incremental",True) #z3.set_param('smt.mbqi.trace',True) @@ -91,7 +93,7 @@ def sorts(name): if name == 'strlit': return z3.StringSort() return None - + #sorts = {} #sorts = {"S":S, # "Int":z3.IntSort()} @@ -102,7 +104,7 @@ def parse_int_params(name): if not all(t.endswith(']') for t in things): raise SyntaxError() return [int(t[:-1]) for t in things] - + def is_solver_sort(name): return name.startswith('bv[') and name.endswith(']') or name == 'int' or name == 'nat' or name == 'strlit' or name.startswith('strbv[') @@ -149,7 +151,7 @@ def clear(): z3_constants = dict() z3_functions = dict() -clear() +clear() #z3_sorts_inv = dict((get_id(z3sort),ivysort) for ivysort,z3sort in z3_sorts.iteritems()) z3_sorts_inv = {} @@ -205,7 +207,7 @@ def lookup_native(thing,table,kind): return z3val def check_native_compat_sym(sym): - table,kind = (relations,"relation") if sym.is_relation() else (functions,"function") + table,kind = (relations,"relation") if sym.is_relation() else (functions,"function") thing = lookup_native(sym,table,kind) # print "check_native_compat_sym: {} {}".format(sym,thing) try: @@ -338,7 +340,7 @@ def lt_pred(sort): sym = ivy_logic.Symbol('<',sort) sig = sym.sort.to_z3() return z3.Function(solver_name(sym), *sig) - + polymacs = { '<=' : lambda s,x,y: z3.Or(x == y,lt_pred(s)(x,y)), '>' : lambda s,x,y: lt_pred(s)(y,x), @@ -424,7 +426,7 @@ def type_constraints(syms): z3_fmla = formula_to_z3_closed(fmla) res.append(z3_fmla) return res - + def clauses_to_z3(clauses): z3_clauses = [conj_to_z3(cl) for cl in clauses.fmlas] @@ -480,7 +482,7 @@ def formula_to_z3(fmla): if len(tcs) > 0: z3_fmla = z3.And(*([z3_fmla] + tcs)) return z3_fmla - + def unsat_core(clauses1, clauses2, implies = None, unlikely=lambda x:False): @@ -594,7 +596,7 @@ def __call__(self,x,y): fact = substitute(self.order,*interp) fact_val = self.model.eval(fact) # print "order: %s = %s" % (fact,fact_val) - return -1 if z3.is_true(fact_val) else 1 + return -1 if z3.is_true(fact_val) else 1 def collect_numerals(z3term): if z3.is_int_value(z3term) or z3.is_bv_value(z3term): @@ -625,7 +627,7 @@ def mine_interpreted_constants(model,vocab): if sort in sort_values: sort_values[sort].update(collect_model_values(sort,model,s)) return dict((x,map(term_to_z3,list(y))) for x,y in sort_values.iteritems()) - + class HerbrandModel(object): def __init__(self,solver,model,vocab): @@ -704,7 +706,7 @@ def eval_to_constant(self,t): def __str__(self): return self.model.sexpr() - + # TODO: need to map Z3 sorts back to ivy sorts def sort_from_z3(s): return z3_sorts_inv[get_id(s)] @@ -756,7 +758,7 @@ def clauses_imply_list(clauses1, clauses2_list): res = [] negs = map(dual_clauses,clauses2_list) - + for clauses2 in negs: z2 = clauses_to_z3(clauses2) # print "check {}".format(clauses2) @@ -1013,7 +1015,7 @@ def get_small_model(clauses, sorts_to_minimize, relations_to_minimize, final_con s = z3.Solver() s.add(clauses_to_z3(clauses)) - + # res = decide(s) # if res == z3.unsat: # return None @@ -1209,7 +1211,7 @@ def filter_redundant_facts(clauses,axioms): "axioms". Currently, this removes only negative formulas that are implied by the positive formulas, so it should work well for facts about total orders, for example. """ - + fmlas = clauses.fmlas pos_fmlas = [fmla for fmla in fmlas if not isinstance(fmla,ivy_logic.Not)] neg_fmlas = [fmla for fmla in fmlas if isinstance(fmla,ivy_logic.Not)] @@ -1324,7 +1326,7 @@ def function_model_to_clauses(h,f): for c in rng.defines(): eq = ivy_logic._eq_lit(fterm,ivy_logic.Constant(ivy_logic.Symbol(c,rng))) # print "function_model_to_clauses: {}".format(eq) - get_lit_facts(h,eq,res) + get_lit_facts(h,eq,res) # non-enumerated function types else: lit = ivy_logic.Literal(1,fun_eq_inst(f)) diff --git a/lib/emacs/ivy-mode.el b/lib/emacs/ivy-mode.el index b62710b2e..846d1d0f9 100644 --- a/lib/emacs/ivy-mode.el +++ b/lib/emacs/ivy-mode.el @@ -87,6 +87,8 @@ "ensure" "around" "parameter" + "globally" + "eventually" ) ) (setq ivy-types '("bool" "int" "bv")) diff --git a/test/test_liveness.ivy b/test/test_liveness.ivy index c0e4efbfb..f2b7175d1 100644 --- a/test/test_liveness.ivy +++ b/test/test_liveness.ivy @@ -27,13 +27,7 @@ object ticket_protocol = { ################################################################################ # - # The protocol itself, together with encoding the fairness - # constraints and the negation of the liveness property - # - # property: forall T:thread. G. pc2(T) -> F. pc3(T) - # fairness: forall T:thread. G. F. last_scheduled(T) - # ~property: exists T:thread. F. (pc2(T) & G. ~pc3(T)) - # Sk(~property): F. (pc2(t0) & G. ~pc3(t0)) + # The protocol description # ################################################################################ @@ -52,10 +46,8 @@ object ticket_protocol = { individual service:ticket individual next_ticket:ticket relation m(T:thread, K:ticket) # use relation and not a function to be in EPR - # individual testfunction(K:ticket):thread # use relation and not a function to be in EPR - individual t0:thread - relation last_scheduled(T:thread) + relation scheduled(T:thread) init pc1(T) init ~pc2(T) @@ -63,48 +55,7 @@ object ticket_protocol = { init service = zero init next_ticket = zero init m(T,K) <-> K = zero - init ~last_scheduled(T) - - # temporal specification - # temporal axiom [fairness] forall T:thread. globally eventually last_scheduled(T) - # temporal property [mutualexclusion] globally forall T1,T2. pc3(T1) & pc3(T2) -> T1 = T2 - # temporal property [nonstravation] forall T:thread. globally (pc2(T) -> eventually pc3(T)) # TODO parsing precedence bug - #temporal property [nonstravation] globally (pc2(t0) -> eventually pc3(t0)) # TODO parsing precedence bug - # temporal property [nonstravation] globally ~(pc2(t0) & globally ~pc3(t0)) # TODO parsing precedence bug - - # proof of nonstravation by l2s { - # conjecture ($l2s_w. (pc2(t0) & (globally ~pc3(t0)))) <-> ~(pc2(t0) & (globally ~pc3(t0))) - # conjecture l2s_frozen -> (pc2(t0) & (globally ~pc3(t0))) - # conjecture l2s_saved -> (pc2(t0) & (globally ~pc3(t0))) - #axiom [fairness] forall T:thread. globally eventually pc1(T) - # temporal axiom [fairness] forall T:thread. globally eventually ( - # (exists K1,K2. after step12(T,K1,K2)) | - # (exists K1. after step12(T,K1)) | - # (exists K1. after step12(T,K1)) | - # (exists K1,K2. after step12(T,K1,K2)) - # ) - # # naming for use in the inductive invariant - # let t0 = nonstravation.T - # let request_flag = pc2(t0) & globally ~pc3(t0) - # let last_scheduled(T) = ( - # (exists K1,K2. after step12(T,K1,K2)) | - # (exists K1. after step12(T,K1)) | - # (exists K1. after step12(T,K1)) | - # (exists K1,K2. after step12(T,K1,K2)) - # ) - # temporal property (forall T:thread. G. F. last_scheduled(T)) -> (forall T:thread. G. pc2(T) -> F. pc3(T)) - # fair action step12 - # fair action step22 - # fair action step23 - # fair action step31 - - # Axioms we may need (not for ticket, in general): - # (forall x. phi) -> (exists x. phi) - # (exists x. eventually phi) -> (eventually exists x. phi) - # - # these may be needed when x isn't in d, and we know forall - # x. eventually phi, and want to wait until (exists x. phi). - + init ~scheduled(T) ################################################################################ # @@ -119,13 +70,12 @@ object ticket_protocol = { action step12(t:thread,k1:ticket, k2:ticket) = { assume pc1(t); assume k1 = next_ticket; - # assume k2 = succ(k1); # bug: succ is in mod.public_actions - assume ~le(k2,k1) & forall Z:ticket. ~le(Z,k1) -> le(k2,Z); + assume k2 = succ(k1); m(t,K) := K = k1; next_ticket := k2; pc1(t) := false; pc2(t) := true; - last_scheduled(T) := T = t; + scheduled(T) := T = t; } action step22(t:thread, k1:ticket) = { @@ -133,7 +83,7 @@ object ticket_protocol = { assume m(t,k1); assume ~le(k1,service); # stay in pc2 - last_scheduled(T) := T = t; + scheduled(T) := T = t; } action step23(t:thread, k1:ticket) = { @@ -142,18 +92,17 @@ object ticket_protocol = { assume le(k1,service); pc2(t) := false; pc3(t) := true; - last_scheduled(T) := T = t; + scheduled(T) := T = t; } action step31(t:thread, k1:ticket, k2:ticket) = { assume pc3(t); assume k1 = service; - # assume k2 = succ(k1); # bug: succ is in mod.public_actions - assume ~le(k2,k1) & forall Z:ticket. ~le(Z,k1) -> le(k2,Z); + assume k2 = succ(k1); service := k2; pc3(t) := false; pc1(t) := true; - last_scheduled(T) := T = t; + scheduled(T) := T = t; } export step12 @@ -167,20 +116,14 @@ object ticket_protocol = { # ################################################################################ - # for testing - # conjecture true | ($l2s_s X. globally eventually ~pc1(X))(Y) - # conjecture true | ($l2s_s X. globally ~globally pc1(X))(Y) - + # 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 - - # safety property - conjecture pc3(T1) & pc3(T2) -> T1 = T2 - # inductive invariant for proving safety conjecture next_ticket = zero -> m(T,zero) conjecture next_ticket ~= zero & m(T,M) -> ~le(next_ticket,M) @@ -192,60 +135,55 @@ object ticket_protocol = { 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 [nonstravation] (forall T:thread. globally (~globally (~last_scheduled(T)))) -> - (globally ~(pc2(t0) & globally ~pc3(t0))) + 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 nonstravation.l2s_waiting - # relation nonstravation.l2s_frozen - # relation nonstravation.l2s_saved + # relation l2s_waiting + # relation l2s_frozen + # relation l2s_saved # - # relation nonstravation.l2s_d_thread(T:thread) - # relation nonstravation.l2s_d_ticket(K:ticket) + # relation l2s_d(X) - polymorphic relation for d + # relation l2s_a(X) - polymorphic relation for a # - # relation nonstravation.l2s_a_thread(T:thread) - # relation nonstravation.l2s_a_ticket(K:ticket) - # - # relation nonstravation.l2s_w[phi] for phi in FO-LTL(original vocabulary) - # relation nonstravation.l2s_wa[A] for A in fair-actions = {step12(T,K1,K2), - # step22(T,K1), - # step23(T,K1), - # step31(T,K1,K2)} - # - # relation nonstravation.l2s_s.pc1(T:thread) - # relation nonstravation.l2s_s.pc2(T:thread) - # relation nonstravation.l2s_s.pc3(T:thread) - # individual nonstravation.l2s_s.service : ticket - # individual nonstravation.l2s_s.next_ticket : ticket - # relation nonstravation.l2s_s.m(T:thread, K:ticket) - # relation nonstravation.l2s_s.[phi] for phi in FO-LTL(original vocabulary) + # 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 are autumatically added - # # conjecture X.l2s_saved -> phi(X.l2s_s) for phi in conjectures over original vocabulary + 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 T. pc3(T))(T1) & ($l2s_s T. pc3(T))(T2) -> T1 = T2 ) 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) ) @@ -255,47 +193,36 @@ object ticket_protocol = { 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 -> (t0 = ($l2s_s. t0)) - - # # basic - # conjecture (forall T:thread. globally ~(globally ~last_scheduled(T))) - conjecture globally ~(globally ~last_scheduled(V0)) - conjecture globally ~(globally ~last_scheduled(T)) # just to try a different variable name - conjecture ~(globally ~last_scheduled(V0)) - conjecture ~(globally ~(pc2(t0) & globally ~pc3(t0))) - conjecture ~($l2s_w. (pc2(t0) & globally ~pc3(t0))) <-> (pc2(t0) & globally ~pc3(t0)) - - - # TODO: should be added automatically - conjecture l2s_waiting | l2s_frozen | l2s_saved - conjecture ~l2s_waiting | ~l2s_frozen - conjecture ~l2s_waiting | ~l2s_saved - conjecture ~l2s_frozen | ~l2s_saved - - - # # basic (but not working) - # conjecture ~(globally (pc2(t0) -> eventually pc3(t0))) - # conjecture eventually (pc2(t0) & globally ~pc3(t0)) - - # conjecture ~($l2s_w. ~(pc2(t0) -> (eventually pc3(t0)))) -> ~(pc2(t0) -> (eventually pc3(t0))) - - # conjecture ($l2s_w. (~(pc2(t0) -> (eventually pc3(t0))))) <-> (~(~(pc2(t0) -> (eventually pc3(t0))))) - # conjecture eventually (pc2(t0) & (globally ~pc3(t0))) - # conjecture ($l2s_w T. (pc2(T) & (globally ~pc3(T))))(t0) -> ~(pc2(t0) & (globally ~pc3(t0))) - # conjecture ~($l2s_w T. (pc2(T) & (globally ~pc3(T))))(t0) -> (pc2(t0) & (globally ~pc3(t0))) - conjecture l2s_frozen -> (pc2(t0) & globally ~pc3(t0)) - conjecture l2s_saved -> (pc2(t0) & globally ~pc3(t0)) - conjecture l2s_saved -> ($l2s_s T,K. m(T,K))(t0,K) <-> m(t0,K) + conjecture l2s_saved -> (sk0 = ($l2s_s. sk0)) + + # basic temporal information + conjecture forall T:thread. globally eventually scheduled(T) + conjecture ~(globally ~(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(t0, 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) @@ -305,49 +232,48 @@ object ticket_protocol = { 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. t0), M) + exists M. ($l2s_s T,K. m(T,K))(($l2s_s. sk0), M) ) - # conjecture that l2s_d is large enough - conjecture l2s_d(t0) + # l2s_d is large enough + conjecture l2s_d(sk0) conjecture ~pc1(T) -> l2s_d(T) conjecture le(K,next_ticket) -> l2s_d(K) - # conjecture that l2s_a is large enough - conjecture ~l2s_waiting -> l2s_a(t0) - conjecture ~l2s_waiting & m(T,K) & m(t0,K0) & ~le(K0,K) & ~pc1(T) -> l2s_a(T) - conjecture ~l2s_waiting & m(t0,K0) & le(K,K0) -> l2s_a(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. last_scheduled(T))(T) -> (($l2s_s T. pc1(T))(T) <-> pc1(T)) - conjecture l2s_saved & ($l2s_w T. last_scheduled(T))(T) -> (($l2s_s T. pc2(T))(T) <-> pc2(T)) - conjecture l2s_saved & ($l2s_w T. last_scheduled(T))(T) -> (($l2s_s T. pc3(T))(T) <-> pc3(T)) - conjecture l2s_saved & ($l2s_w T. last_scheduled(T))(T) -> (($l2s_s T,K. m(T,K))(T,K) <-> m(T,K)) + 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. last_scheduled(X))(T) & - ($l2s_s T. pc2(T))(T) & - m(T,K) & - m(t0,K0) + 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)) + (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. last_scheduled(T))(T) & - ($l2s_s T. pc3(T))(T) & - m(T,K) & - m(t0,K0) + 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)) + (pc1(T) & K = ($l2s_s. service) & ~le(service, ($l2s_s. service))) | + (pc2(T) & ~le(K,K0)) ) } } with this - }