зеркало из https://github.com/microsoft/ivy.git
446 строки
13 KiB
XML
446 строки
13 KiB
XML
#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
|
|
|
|
|
|
|