#lang ivy1.7

################################################################################
#
# TODO: 
#
################################################################################

isolate proc = {
 type t

 object impl = {
   interpret proc.t->bv[1] 
 }
    attribute test=impl
}

isolate data_type = {
 type t

 object impl = {
   interpret data_type.t->bv[1] 
 }
    attribute test=impl
}

isolate addr_type = {
 type t

 object impl = {
   interpret addr_type.t->bv[1] 
 }
    attribute test=impl
}

isolate ltime = {
    type t

    relation (X:t < Y:t)
    action incr(inp:t) returns (out:t)

    object spec = {
	property X:t < Y & Y < Z -> X < Z
	property ~(X:t < Y & Y < X)
	property X:t < Y | X = Y | Y < X

        after incr {
            assume inp < out
        }
    }

    object impl = {
	interpret ltime.t->bv[8]
        implement incr {
            out := inp + 1
        }
    }
    attribute test=impl
}

isolate gtime = {
    type t

    relation (X:t < Y:t)
    action incr(inp:t) returns (out:t)

    object spec = {
	property X:t < Y & Y < Z -> X < Z
	property ~(X:t < Y & Y < X)
	property X:t < Y | X = Y | Y < X

        after incr {
            assume inp < out
        }
    }

    object impl = {
	interpret gtime.t->bv[8]
    }
    attribute test=impl
}

type op_type = {nop,ld,st,lda,stl}

module evs_type = {
   individual p       : proc.t
   individual op      : op_type
   individual addr    : addr_type.t
   individual data    : data_type.t

   individual serialized : bool

   individual time    : gtime.t
}

################################################################################
# Specification: 
################################################################################

object ref = {

 instantiate evs(T:ltime.t) : evs_type

################################################################################
# current global time

 individual  gt : gtime.t

################################################################################
# global memory state 

  individual mem(A:addr_type.t) : data_type.t

################################################################################
# event T1 prevents T2 if it must come before T2 according to the
# ordering conditions but is not yet serialized. The definition
# here is strong enough to imply release consistency (ld and
# st to different addresses commute, but nothing commutes with
# stl and lda)
#
#    P1) only one of ld, lda, st, stl pending for same address from same processor
#
# An acquire synchronization must ensure that no younger load/store executes before the
# acquire is complete
#
# => A1) prevent lda to issue until all older ld*/st* are finished to ensure it
#        doesn't overtake those 
#    A2) prevent younger ld*/st* to issue before lda
#
# A release synchronization must ensure that all older loads/stores complete before the
# release is issued.
#
# => R1) prevent stl to issue until all older ld*/st* are finished to ensure it
#        doesn't overtake those
#
#  P0 1) st         P1 1) ld
#  P0 2) stl        P1 2) lda
#
# Acquires and releases must execute atomically with respect to one another
#

relation   prevents(T1:ltime.t,T2:ltime.t)
definition prevents(T1,T2) = ~evs(T1).serialized 
     	                   & (T1 < T2) & (evs(T1).op=ld | evs(T1).op=lda | evs(T1).op=st | evs(T1).op=stl)
    	                   & evs(T1).p = evs(T2).p
    	                   & (evs(T1).addr = evs(T2).addr | evs(T2).op = stl | evs(T2).op = lda)

action create(lt:ltime.t,p:proc.t,op:op_type,a:addr_type.t,d:data_type.t) = {
  evs(lt).p          := p;
  evs(lt).op         := op;
  evs(lt).addr       := a;
  evs(lt).data       := d;
  evs(lt).serialized := false;
}

action perform(p:proc.t, lt:ltime.t) = {
  var a : addr_type.t;
  var d : data_type.t;

# serialization must be appropriately ordered

  assert ~prevents(T,lt);

# serialize at current global time
  evs(lt).serialized := true;
  evs(lt).time       := gt;
  evs(lt).op         := nop;

  # advance global time
    gt := gt.incr();

# update the global memory state

     a := evs(lt).addr;
     d := evs(lt).data;

     if evs(lt).op = ld | evs(lt).op = lda {
	evs(lt).data := mem(a)
     } else if evs(lt).op = st | evs(lt).op = stl {
	mem(a) := d
     }			
  }

}

################################################################################
# arm: 
################################################################################
type arm_ph_type = {arm_idle_ph, arm_st_ph, arm_stl_ph, arm_ld_ph, arm_lda_ph, arm_rsp_ph, arm_rspa_ph, arm_st_isd_ph, arm_ld_isd_ph, arm_stl_isd_ph, arm_lda_isd_ph}

object arm = {
 relation pnd_st(P:proc.t, A:addr_type.t, T:ltime.t)
 relation pnd_stl(P:proc.t, A:addr_type.t, T:ltime.t)
 relation pnd_ld(P:proc.t, A:addr_type.t, T:ltime.t)
 relation pnd_lda(P:proc.t, A:addr_type.t, T:ltime.t)

 relation isd_st(P:proc.t, A:addr_type.t, T:ltime.t)
 relation isd_stl(P:proc.t, A:addr_type.t, T:ltime.t)
 relation isd_ld(P:proc.t, A:addr_type.t, T:ltime.t)
 relation isd_lda(P:proc.t, A:addr_type.t, T:ltime.t)

 individual lt : ltime.t

 action step(p:proc.t, ph:arm_ph_type, a:addr_type.t,d:data_type.t,t:ltime.t) = {

     if ph=arm_st_ph {
          if forall T. ~(pnd_ld(p,a,T) | pnd_lda(p,a,T) | pnd_st(p,a,T) | pnd_stl(p,a,T)) { # P1
            if forall A. forall T. ~pnd_lda(p,A,T) { # A2
               pnd_st(p,a,lt) := true;
               isd_st(p,a,lt) := true;

               call dcs.st(p,a,d);
               call ref.create(lt,p,st,a,d);
               call ref.perform(p,lt);

               pnd_st(p,a,lt) := false;
               isd_st(p,a,lt) := false;
            } else {
               pnd_st(p,a,lt) := true;
               isd_st(p,a,lt) := false;
            };

            lt := lt.incr();
          }
     } else if ph=arm_st_isd_ph {
          if pnd_st(p,a,t) {
             if ~isd_st(p,a,t) {
                 if forall A. forall T. ~pnd_lda(p,A,T) | t<T { # A2
                    isd_st(p,a,t) := true;

                    call dcs.st(p,a,d);
                    call ref.create(t,p,st,a,d);
                    call ref.perform(p,t);

                    pnd_st(p,a,t) := false;
                    isd_st(p,a,t) := false;
                 }
             }
          }
     } else if ph=arm_stl_ph {
          if forall T. ~(pnd_ld(p,a,T) | pnd_lda(p,a,T) | pnd_st(p,a,T) | pnd_stl(p,a,T)) { # P1
            if forall A. forall T. ~(pnd_ld(p,A,T) | pnd_lda(p,A,T) | pnd_st(p,A,T) | pnd_stl(p,A,T)) { # R1
               pnd_stl(p,a,lt)      := true;
               isd_stl(p,a,lt)      := true;

               call dcs.st(p,a,d);
               call ref.create(lt,p,stl,a,d);

               call ref.perform(p,lt);

               pnd_stl(p,a,lt) := false;
               isd_stl(p,a,lt) := false;
            } else {
               pnd_stl(p,a,lt)      := true;
               isd_stl(p,a,lt)      := false;
            };

            lt := lt.incr();
	  }
     } else if ph=arm_stl_isd_ph {
          if pnd_stl(p,a,t) {
             if ~isd_stl(p,a,t) {
                 if forall A. forall T. ~(pnd_ld(p,A,T) | pnd_lda(p,A,T) | pnd_st(p,A,T) | pnd_stl(p,A,T)) | t<T | t=T { # R1
                    isd_stl(p,a,t) := true;

                    call dcs.st(p,a,d);
                    call ref.create(t,p,stl,a,d);
                    call ref.perform(p,t);

                    pnd_stl(p,a,t) := false;
                    isd_stl(p,a,t) := false;
                 }
             }
          }
     } else if ph=arm_ld_ph {
          if forall T. ~pnd_ld(p,a,T) & ~pnd_lda(p,a,T) & ~pnd_st(p,a,T) & ~pnd_stl(p,a,T) { # P1
            if forall A. forall T. ~pnd_lda(p,A,T) { # A2
               pnd_ld(p,a,lt)      := true;
               isd_ld(p,a,lt)      := true;

               call ref.create(lt,p,ld,a,d);
            } else {
               pnd_ld(p,a,lt) := true;
               isd_ld(p,a,lt) := false;
            };

            lt := lt.incr();
	  }
     } else if ph=arm_ld_isd_ph {
          if pnd_ld(p,a,t) {
             if ~isd_ld(p,a,t) {
                 if forall A. forall T. ~pnd_lda(p,A,T) | t<T { # A2
                    isd_ld(p,a,t) := true;
                    call ref.create(t,p,ld,a,d);
                 }
             }
          }
     } else if ph=arm_lda_ph {
          if forall T. ~pnd_ld(p,a,T) & ~pnd_lda(p,a,T) & ~pnd_st(p,a,T) & ~pnd_stl(p,a,T) { # P1
            if forall A. forall T. ~pnd_lda(p,A,T) & ~pnd_ld(p,A,T) & ~pnd_st(p,A,T) & ~pnd_stl(p,A,T) { # A1
              pnd_lda(p,a,lt)      := true;
              isd_lda(p,a,lt)      := true;

              call ref.create(lt,p,lda,a,d);
            } else {
              pnd_lda(p,a,lt)      := true;
              isd_lda(p,a,lt)      := false;
            };

            lt := lt.incr();
	  }
     } else if ph=arm_lda_isd_ph {
          if pnd_lda(p,a,t) {
             if ~isd_lda(p,a,t) {
                 if forall A. forall T. ~pnd_lda(p,A,T) & ~pnd_ld(p,A,T) & ~pnd_st(p,A,T) & ~pnd_stl(p,A,T) | t<T | t=T { # A2
                    isd_lda(p,a,t) := true;
                    call ref.create(t,p,lda,a,d);
                 }
             }
          }
     }
  }

# receive ld response and check the value against the expected value

 action recv(ph:arm_ph_type, p:proc.t, a:addr_type.t, t:ltime.t) = {

   if ph=arm_rsp_ph {

      if isd_ld(p,a,t) {

      call ref.perform(p,t);

      pnd_ld(p,a,t)      := false;
      isd_ld(p,a,t)      := false;
     }
   } else if ph=arm_rspa_ph {

      if isd_lda(p,a,t) {

      call ref.perform(p,t);

      pnd_lda(p,a,t)      := false;
      isd_lda(p,a,t)      := false;
     }
   }
 }
}

################################################################################
# DCS+DRAM
################################################################################

object dcs = {

 individual data(A:addr_type.t) : data_type.t

 action st(p:proc.t, a:addr_type.t, d:data_type.t) = {
  data(a) := d;
 }

 action ld(a:addr_type.t) returns (d:data_type.t)  = {
  d := data(a)
 }

}

# instantiate model: processors, network, and memory

# initialize the state to nothing outstanding

after init {
 arm.pnd_st(P,A,T)      := false;
 arm.pnd_stl(P,A,T)     := false;
 arm.pnd_ld(P,A,T)      := false;
 arm.pnd_lda(P,A,T)     := false;

 arm.isd_st(P,A,T)      := false;
 arm.isd_stl(P,A,T)     := false;
 arm.isd_ld(P,A,T)      := false;
 arm.isd_lda(P,A,T)     := false;

 ref.evs(T).op          := nop;

 ref.evs(T).serialized  := false;
}

# zero

# 

conjecture ~arm.isd_st(P,A,T)
conjecture ~arm.isd_stl(P,A,T)

conjecture (arm.pnd_st(P,A,T)  & arm.isd_st(P,A,T))  <-> (ref.evs(T).p=P & ref.evs(T).op=st  & ref.evs(T).addr=A)
conjecture (arm.pnd_stl(P,A,T) & arm.isd_stl(P,A,T)) <-> (ref.evs(T).p=P & ref.evs(T).op=stl & ref.evs(T).addr=A)
conjecture (arm.pnd_ld(P,A,T)  & arm.isd_ld(P,A,T))  <-> (ref.evs(T).p=P & ref.evs(T).op=ld  & ref.evs(T).addr=A)
conjecture (arm.pnd_lda(P,A,T) & arm.isd_lda(P,A,T)) <-> (ref.evs(T).p=P & ref.evs(T).op=lda & ref.evs(T).addr=A)

conjecture arm.pnd_st(P,A,T)  -> (T < arm.lt)
conjecture arm.pnd_stl(P,A,T) -> (T < arm.lt)
conjecture arm.pnd_ld(P,A,T)  -> (T < arm.lt)
conjecture arm.pnd_lda(P,A,T) -> (T < arm.lt)

conjecture (arm.pnd_st(P,A,T1)  & arm.pnd_st(P,A,T2))  -> T1=T2
conjecture (arm.pnd_stl(P,A,T1) & arm.pnd_stl(P,A,T2)) -> T1=T2
conjecture (arm.pnd_ld(P,A,T1)  & arm.pnd_ld(P,A,T2))  -> T1=T2
conjecture (arm.pnd_lda(P,A,T1) & arm.pnd_lda(P,A,T2)) -> T1=T2

conjecture ~(arm.pnd_ld(P,A,T1)  & arm.pnd_st(P,A,T2))
conjecture ~(arm.pnd_ld(P,A,T1)  & arm.pnd_stl(P,A,T2))
conjecture ~(arm.pnd_ld(P,A,T1)  & arm.pnd_lda(P,A,T2))
conjecture ~(arm.pnd_lda(P,A,T1) & arm.pnd_st(P,A,T2))
conjecture ~(arm.pnd_lda(P,A,T1) & arm.pnd_stl(P,A,T2))
conjecture ~(arm.pnd_st(P,A,T1)  & arm.pnd_stl(P,A,T2))

conjecture arm.isd_st(P,A,T)  -> arm.pnd_st(P,A,T)
conjecture arm.isd_stl(P,A,T) -> arm.pnd_stl(P,A,T)
conjecture arm.isd_ld(P,A,T)  -> arm.pnd_ld(P,A,T)
conjecture arm.isd_lda(P,A,T) -> arm.pnd_lda(P,A,T)

# When lda is issued there are no older ld, lda, st, stl pending

conjecture arm.isd_lda(P,A,T) -> ~((arm.pnd_ld(P,A1,T1) | arm.pnd_lda(P,A1,T1) | arm.pnd_st(P,A1,T1) | arm.pnd_stl(P,A1,T1)) & T1<T)

# When lda is issued there are no younger ld, lda, st, stl issued

conjecture arm.pnd_lda(P,A,T) -> ~((arm.isd_ld(P,A1,T1) | arm.isd_lda(P,A1,T1) | arm.isd_st(P,A1,T1) | arm.isd_stl(P,A1,T1)) & T1>T)

conjecture  (arm.pnd_ld(P1,A1,T1)  & arm.pnd_ld(P2,A2,T2)  & T1=T2) -> (P1=P2 & A1=A2)
conjecture ~(arm.pnd_ld(P1,A1,T1)  & arm.pnd_lda(P2,A2,T2) & T1=T2)
conjecture ~(arm.pnd_ld(P1,A1,T1)  & arm.pnd_st(P2,A2,T2)  & T1=T2)
conjecture ~(arm.pnd_ld(P1,A1,T1)  & arm.pnd_stl(P2,A2,T2) & T1=T2)
conjecture  (arm.pnd_lda(P1,A1,T1) & arm.pnd_lda(P2,A2,T2) & T1=T2) -> (P1=P2 & A1=A2)
conjecture ~(arm.pnd_lda(P1,A1,T1) & arm.pnd_st(P2,A2,T2)  & T1=T2)
conjecture ~(arm.pnd_lda(P1,A1,T1) & arm.pnd_stl(P2,A2,T2) & T1=T2)
conjecture  (arm.pnd_st(P1,A1,T1)  & arm.pnd_st(P2,A2,T2) & T1=T2)  -> (P1=P2 & A1=A2)
conjecture ~(arm.pnd_st(P1,A1,T1)  & arm.pnd_stl(P2,A2,T2) & T1=T2)
conjecture  (arm.pnd_stl(P1,A1,T1) & arm.pnd_stl(P2,A2,T2) & T1=T2) -> (P1=P2 & A1=A2)

export arm.step
export arm.recv