ivy

gistfile1.txt

#lang ivy2
#Panda's synchronization protocol

# General modules & macros
#Functional dependencies
module lone(f) = {
 axiom (f(X, Y1) & f(X, Y2)) -> Y1 = Y2
}

module injective(f) = {
 axiom (f(X1, Y) & f(X2, Y)) -> X1 = X2
}

macro assign_empty(f, a) = { # f(a) := {}
  f(a, X) := false
  }
macro assign_value(f, a, v ) = { # f(a) := {v}
  f(a, X) :=  X = v
  }


type transaction
type node
type time
type key
type operation


relation before(X:time, Y:time)
axiom before(X, X) # Reflexive
axiom before(X, Y) & before(Y, Z) -> before(X, Z) # Transitive
axiom before(X, Y) & before(Y, X) -> X = Y # Anti-symmetric
axiom before(X, Y) | before(Y, X) # total
individual zero:time
axiom before(zero, X)

# Advance time
macro assume_next(a, b) = {
      assume before(a, b) ;
      assume a ~= b;
      assume before(a, Y)  & a ~= Y  -> before(b, Y)
      }


relation commit_time(X: transaction, T: time)  # Commit time for transaction

instantiate lone(commit_time)

instantiate injective(commit_time)
axiom commit_time(Tx, T) -> T ~= zero


relation op_in_tx(Tx : transaction, Op: operation) # An operation of transaction is op

relation next_operation(Tx: transaction, Op1 : operation, Op2 : operation) # The next operation within the transaction

axiom next_operation(Tx, Op, Op1) & next_operation(Tx, Op, Op2) -> Op1 = Op2 # Unique successor

axiom next_operation(Tx, Op1, Op) & next_operation(Tx, Op2, Op) -> Op1 = Op2 # Unique predecessor

# Each operation reads and writes one key
relation op_reads_key(Op: operation, K: key) # OP reads k
instantiate lone(op_reads_key) # See if we can remove this.
relation op_writes_key(Op : operation, K: key) # OP writes k
instantiate lone(op_reads_key) # See if we can remove this

# Do not read and write the same key.
axiom op_reads_key(Op, K) & op_writes_key(Op, K2) -> K1 ~= K2

# The operation in each node
relation op_node(Op: operation, N : node) # The node on which an operation is applied
instantiate lone(op_node)

axiom op_in_tx(T, O1) & op_in_tx(T, O2) & O1 ~= O2 & op_node(O1, N1) & op_node(O2, N2) -> N1 ~= N2
# Each op is in a single Tx.
instantiate injective(op_in_tx)

relation precommit_tx(Tx : transaction, N: node) # Is transaction tx precommitted at n
relation abort_tx(Tx : transaction)

relation commit_tx(Tx: transaction) # Is tx committed
relation depends_tx(Tx: transaction, K: key, T : time) #Flow values between commited transactions

init ~depends_tx(Tx, K, T) # Empty depends
axiom depends_tx(Tx, K, T) & commit_time(Tx, T1) -> before(T, T1)

relation write_tx(Tx: transaction, K: key)
init ~write_tx(Tx, K)

relation node_for_key(K: key,  N : node) # Key is at node n
instantiate lone(node_for_key)

relation last_committed_key_write_time(K: key, T: time) # Last time k was written (commit)
instantiate lone(last_committed_key_write_time)
init last_committed_key_write_time(K, zero)

relation last_committed_key_read_time(K: key, T: time) # Last time k was read (commit)
instantiate lone(last_committed_key_read_time)
init last_committed_key_read_time(K, zero)

relation last_uncommitted_key_write_time(K: key, T: time) # Last time k was written (uncommit)
instantiate lone(last_uncommitted_key_write_time)
init last_uncommitted_key_write_time(K, zero)

relation last_uncommitted_key_read_time(K: key, T: time) # Last time k was read (uncommit)
instantiate lone(last_uncommitted_key_read_time)
init last_uncommitted_key_read_time(K, zero)

# Constraints
axiom ~abort_tx(Tx) | ~commit_tx(Tx) # Abort and commit are disjoint

axiom op_reads_key(Op, K) & node_for_key(K, N1)  & op_node(Op, N2) -> N1 = N2  #Operations must be local
axiom op_writes_key(Op, K) & node_for_key(K, N1) &  op_node(Op, N2) -> N1 = N2 #Operations must be local


axiom last_uncommitted_key_write_time(K, T1) & last_committed_key_write_time(K, T2) -> before(T2, T1)
axiom last_uncommitted_key_read_time(K, T1) & last_committed_key_read_time(K, T2) -> before(T2, T1)

# Transaction protocol

individual tx: transaction
individual op: operation, op1: operation, op2: operation
individual n : node, np: node
individual t1: time, t2: time, t3: time, t4: time
individual kw: key, kr: key

action transaction = {
  tx := *;
  op := *;
  op1 := *;
  op2 := *;
  n := *;
  np := *;
  t1 := *;
  t2 := *;
  t3 := *;
  t4 := *;
  kw := *;
  kr := *;
  assume op_in_tx(tx, op) ; # Grab an operation
  assume ~abort_tx(tx); # Ensures that the transaction is not already aborted
  assume ~next_operation(tx, X, op) | # First operation
        (next_operation(tx, op1, op) &  
		op_node(op1, np) & 
		precommit_tx(tx, np)) ;
                   # Ensures that the previous operation was successfully
  assume op_node(op, n) ; # Assume operation is in node n
  assume ~precommit_tx(tx, n);
  assume ~op_writes_key(op, K) | 
	(op_writes_key(op, kw) &
	 node_for_key(kw, n));

  assume ~op_reads_key(op, K) |
	(op_reads_key(op, kr) &
	 node_for_key(kr, n));
  
  assume commit_time(tx, t1); 

  if (op_writes_key(op, kw) &
      last_uncommitted_key_write_time(kw, t2) &
      last_uncommitted_key_read_time(kw, t3) &
      (before(t1, t2) | before(t1, t3))) {
      	  abort_tx(tx) := true
  } else {
    if (op_writes_key(op, kw)) {
      last_uncommitted_key_write_time(kw, T) := T = t1
    } else {
      if (op_reads_key(op, kr) &
      	last_uncommitted_key_write_time(kr, t3) &
      	last_committed_key_write_time(kr, t4) &
      	t3 ~= t4 &
      	before(t3, t1)) {
      	abort_tx(tx) := true
      } else {
      	if (op_reads_key(op, kr)) {
      	  last_uncommitted_key_read_time(kr, T) := T = t1;
      	  precommit_tx(tx, n) := true
      	  #if * {
      	  #  assume ~next_operation(tx, op, Op2);
      	  #  commit_tx(tx) := true
          #}
        }
      }
    }
  }
}

individual tx1: transaction, tx2: transaction
individual k: key
individual n1: node, n2: node
action error = {
# Local serializability should always hold
     tx1 := *;
     tx2 := *;
     k := *;
     n1 := *;
     n2 := *;
     t1 := *;
     t2 := *;
     t3 := *;
     assume(tx1 ~= tx2 &
            commit_tx(tx1) &
            commit_tx(tx2)  &
            commit_time(tx1, t1) &
            commit_time(tx2, t2) &
            before(t1,t2) &
            write_tx(tx1, k) &
            depends_tx(tx2, k, t3) & # tx2 read k, k was updated at time t1
            ~before(t3, t1))
   }