Added example "migration" (Bouhadiba et al, Emsoft 2011)
Gwenaël Delaval
12 years ago
parent
ce2e2bdcd0
commit
d193d3320b
@ -0,0 +1,103 @@
|
||||
|
||||
SIM_PROG=migration
|
||||
# same as SIM_PROG, capitalized
|
||||
SIM_MOD=Migration
|
||||
SIM_NODE=main
|
||||
|
||||
# This generic Makefile does not allow contract and simulated node in
|
||||
# two different modules (can be two different nodes, though)
|
||||
CONTRACT_PROG=$(SIM_PROG)
|
||||
CONTRACT_MOD=$(SIM_MOD)
|
||||
CONTRACT_NODE=main
|
||||
|
||||
CC=gcc
|
||||
HEPTC=heptc -hepts
|
||||
HEPTS=hepts
|
||||
SIGALI=sigali
|
||||
|
||||
HEPT_LIB_C=/usr/local/lib/heptagon/c
|
||||
|
||||
CTRLR_PROG=$(CONTRACT_NODE)_controller
|
||||
|
||||
HEPT_PATH=$(shell pwd)
|
||||
|
||||
# Path to C headers
|
||||
HEPT_CINCLUDES=
|
||||
CFLAGS= $(HEPT_CINCLUDES) -I $(CTRLR_PROG)_c -I $(HEPT_LIB_C)
|
||||
|
||||
|
||||
HEPT_SOURCES = $(wildcard *.ept)
|
||||
HEPT_MODNAMES = $(patsubst %.ept,%,$(HEPT_SOURCES))
|
||||
|
||||
HEPT_C_FILES = $(shell echo $(HEPT_SOURCES) | sed -r 's+([^ ]*).ept+\1_c/\1.c+g')
|
||||
#HEPT_C_FILES = $(patsubst %.ept,%_c/%.c,$(HEPT_SOURCES))
|
||||
HEPT_C_DIRS = $(patsubst %.ept,%_c,$(HEPT_SOURCES))
|
||||
HEPT_Z3Z_DIRS = $(patsubst %.ept,%_z3z,$(HEPT_SOURCES))
|
||||
HEPT_OBJS = $(HEPT_C_FILES:.c=.o)
|
||||
|
||||
CFLAGS += $(patsubst %, -I %,$(HEPT_C_DIRS))
|
||||
|
||||
|
||||
# define NODES_template
|
||||
# NODES_$(2) = $$(shell grep \\bnode\\b $(1) | sed -r 's/^.*node ([a-zA-Z0-9_]*)[^a-zA-Z0-9_].*$$$$/\1/g')
|
||||
|
||||
# Z3Z_FILES_$(2) = $$(patsubst %,$(2)_z3z/%.z3z,$$(NODES_$(2)))
|
||||
# HEPT_Z3Z_FILES += $$(Z3Z_FILES_$(2))
|
||||
# HEPT_Z3Z_DIRS += $(2)_z3z
|
||||
# endef
|
||||
|
||||
|
||||
# $(foreach ept,$(HEPT_SOURCES),$(eval $(call NODES_template,$(ept),$(shell basename $(ept) .ept))))
|
||||
|
||||
|
||||
CTRLR_C_FILES = $(CTRLR_PROG)_c/$(CTRLR_PROG).c
|
||||
CTRLR_OBJS = $(CTRLR_C_FILES:.c=.o)
|
||||
|
||||
all: sim
|
||||
|
||||
sim: $(SIM_NODE)_sim $(SIM_PROG).epci
|
||||
$(HEPTS) -mod $(SIM_MOD) -node $(SIM_NODE) -exec ./$(SIM_NODE)_sim
|
||||
|
||||
$(SIM_NODE)_sim: $(SIM_PROG)_c/_main.o $(HEPT_OBJS) $(CTRLR_OBJS)
|
||||
$(CC) $(LDFLAGS) -o $(SIM_NODE)_sim $^
|
||||
|
||||
# define HEPT_template
|
||||
# $(1).epci $$(C_FILES_$(1)) $(1): $(1).ept
|
||||
# hec -target c $(1).ept
|
||||
# endef
|
||||
|
||||
# $(foreach ept,$(HEPT_SOURCES), $(eval $(call HEPT_template,$(shell basename $(ept) .ept))))
|
||||
|
||||
$(CONTRACT_PROG)_z3z/$(CONTRACT_NODE).z3z: $(CONTRACT_PROG).ept
|
||||
$(HEPTC) -target c -target z3z -s $(SIM_NODE) $(CONTRACT_PROG).ept
|
||||
|
||||
$(CONTRACT_PROG).epci \
|
||||
$(CONTRACT_PROG)_c/$(CONTRACT_PROG).c \
|
||||
$(CONTRACT_PROG)_c/_main.c: $(CONTRACT_PROG)_z3z/$(CONTRACT_NODE).z3z
|
||||
|
||||
# %.epci %_c/%.c: %.ept
|
||||
# $(HEPTC) -target c $<
|
||||
|
||||
%.epci: %.epi
|
||||
$(HEPTC) $<
|
||||
|
||||
$(CTRLR_PROG).ept: $(CONTRACT_PROG)_z3z/$(CONTRACT_NODE).z3z
|
||||
$(SIGALI) < $(CONTRACT_PROG)_z3z/$(CONTRACT_NODE).z3z
|
||||
|
||||
$(CTRLR_PROG).epci $(CTRLR_PROG)_c/$(CTRLR_PROG).c: $(CTRLR_PROG).ept
|
||||
$(HEPTC) -target c $(CTRLR_PROG).ept
|
||||
|
||||
%.o: %.c
|
||||
$(CC) -c $(CFLAGS) $< -o $@
|
||||
|
||||
clean:
|
||||
rm -fr $(HEPT_C_DIRS) $(HEPT_Z3Z_DIRS) $(HEPT_JAVA_DIRS)
|
||||
rm -f $(SIM_NODE)_sim main.*
|
||||
rm -f *.epci *.mls *.ml *.obc ./*~
|
||||
rm -f $(CTRLR_PROG).ept
|
||||
|
||||
# Dependences
|
||||
|
||||
#provadm.epci $(C_FILES_provadm) provadm: provadm_ctrl.epci
|
||||
|
||||
$(HEPT_OBJS) $(SIM_PROG)_c/_main.o: $(CTRLR_C_FILES)
|
||||
@ -0,0 +1,500 @@
|
||||
(*
|
||||
V2 +
|
||||
In this example we model is a falttering of the example toy.
|
||||
we may add some lifecycle management.
|
||||
*)
|
||||
|
||||
type core = C1| C2| C3| C4
|
||||
|
||||
|
||||
|
||||
|
||||
(* An automaton to model the lifecycyle of a component *)
|
||||
node lifecycle(change, kill, fifoEmpty :bool) returns(started, unbound:bool; c_start, c_connect, c_stop, c_disconnect:bool)
|
||||
let
|
||||
automaton
|
||||
state STOPPED do
|
||||
started = false;
|
||||
unbound = true;
|
||||
(c_start, c_connect, c_stop, c_disconnect)=(change, change, false, false);
|
||||
until change then STARTED
|
||||
|
||||
|
||||
state STARTED do
|
||||
started = true;
|
||||
unbound = false;
|
||||
(c_start, c_connect, c_stop, c_disconnect)=(false, false, (change&fifoEmpty)or(kill),(change or kill));
|
||||
until change & not fifoEmpty then STOPPING
|
||||
| change & fifoEmpty then STOPPED
|
||||
| kill then STOPPED
|
||||
|
||||
state STOPPING do
|
||||
started = true;
|
||||
unbound = true;
|
||||
(c_start, c_connect, c_stop, c_disconnect)=(false, change, (fifoEmpty or kill), false);
|
||||
until fifoEmpty or kill then STOPPED
|
||||
| change then STARTED
|
||||
end;
|
||||
tel
|
||||
|
||||
(* An atamaton to model the state of a FIFIO *)
|
||||
node fifo(f:bool) returns (full:bool)
|
||||
let
|
||||
automaton
|
||||
state EMPTY do
|
||||
full = false;
|
||||
until f then FULL
|
||||
state FULL do
|
||||
full = true;
|
||||
until not f then EMPTY
|
||||
end;
|
||||
tel
|
||||
|
||||
|
||||
(* defines the position of a task *)
|
||||
(* It has two boolean inputs to encode 4 possible outgoing transitions *)
|
||||
|
||||
node position(a, b :bool)returns(position:core; c_mig1, c_mig2, c_mig3, c_mig4:bool)
|
||||
|
||||
(* !a!b go to the next in the numerical order
|
||||
!ab to the second
|
||||
a!b to the last *)
|
||||
let
|
||||
|
||||
automaton
|
||||
state C1 do
|
||||
position=C1;
|
||||
(c_mig1, c_mig2, c_mig3, c_mig4)=(false, not a & not b, not a & b, a & not b);
|
||||
until not a & not b then C2
|
||||
| not a & b then C3
|
||||
| a & not b then C4
|
||||
|
||||
state C2 do
|
||||
position=C2;
|
||||
(c_mig1, c_mig2, c_mig3, c_mig4)=(a & not b, false, not a & not b, not a & b);
|
||||
until not a & not b then C3
|
||||
| not a & b then C4
|
||||
| a & not b then C1
|
||||
|
||||
state C3 do
|
||||
position=C3;
|
||||
(c_mig1, c_mig2, c_mig3, c_mig4)=( not a & b, a & not b, false, not a & not b);
|
||||
until not a & not b then C4
|
||||
| not a & b then C1
|
||||
| a & not b then C2
|
||||
|
||||
|
||||
state C4 do
|
||||
position=C4;
|
||||
(c_mig1, c_mig2, c_mig3, c_mig4)=( not a & not b, not a & b, a & not b, false);
|
||||
until not a & not b then C1
|
||||
| not a & b then C2
|
||||
| a & not b then C3
|
||||
end;
|
||||
tel
|
||||
|
||||
|
||||
|
||||
(* core availability in the paper it's called proc *)
|
||||
node core_mode(disable:bool)returns(active:bool)
|
||||
let
|
||||
automaton
|
||||
state COREON do
|
||||
active= true;
|
||||
until disable then COREOFF
|
||||
|
||||
state COREOFF do
|
||||
active= false;
|
||||
until not disable then COREON
|
||||
end;
|
||||
tel
|
||||
|
||||
|
||||
(* computes the communication cost associated with each core hosting the tasks *)
|
||||
(* in the paper there is additional inputs f: frequency c: function cost *)
|
||||
|
||||
node communication_cost(core1, core2:core)returns(costcpu1, costcpu2:int)
|
||||
var sameproc, samecore:bool;
|
||||
task1_cpu, task1_core, task2_cpu, task2_core:bool;
|
||||
let
|
||||
|
||||
switch core1
|
||||
| C1 do (task1_cpu, task1_core)=(false, false)
|
||||
| C2 do (task1_cpu, task1_core)=(false, true);
|
||||
| C3 do (task1_cpu, task1_core)=(true, false);
|
||||
| C4 do (task1_cpu, task1_core)=(true, true);
|
||||
end ;
|
||||
|
||||
switch core2
|
||||
| C1 do (task2_cpu, task2_core)=(false, false)
|
||||
| C2 do (task2_cpu, task2_core)=(false, true);
|
||||
| C3 do (task2_cpu, task2_core)=(true, false);
|
||||
| C4 do (task2_cpu, task2_core)=(true, true);
|
||||
end ;
|
||||
|
||||
sameproc = (task1_cpu & task2_cpu) or (not task1_cpu & not task2_cpu);
|
||||
samecore = sameproc & ((task1_core & task2_core) or (not task1_core & not task2_core));
|
||||
|
||||
(costcpu1, costcpu2)= if samecore then (10,20)
|
||||
else if sameproc then (20,40)
|
||||
else (50,100);
|
||||
tel
|
||||
|
||||
|
||||
(* associates the cost to the given coreId *)
|
||||
node core_cost(coreId:core; cost:int)returns(c1, c2, c3, c4:int)
|
||||
let
|
||||
switch coreId
|
||||
| C1 do (c1,c2,c3,c4)= (cost, 0,0,0)
|
||||
| C2 do (c1,c2,c3,c4)= (0,cost,0,0)
|
||||
| C3 do (c1,c2,c3,c4)= (0,0,cost,0)
|
||||
| C4 do (c1,c2,c3,c4)= (0,0,0,cost);
|
||||
end;
|
||||
tel
|
||||
|
||||
(* modeling asynchronous commands *)
|
||||
node command(start, isdone: bool)returns(pending:bool)
|
||||
let
|
||||
automaton
|
||||
state DONE do
|
||||
pending = false;
|
||||
until start then PENDING
|
||||
|
||||
state PENDING do
|
||||
pending=true;
|
||||
until isdone then DONE
|
||||
end;
|
||||
tel
|
||||
|
||||
|
||||
(* ======================================== some utility nodes ============================================= *)
|
||||
|
||||
|
||||
|
||||
|
||||
(* retruns an integer representation of the coreId*)
|
||||
node compute_core(coreId:core; active:bool)returns(icore:int)
|
||||
let
|
||||
|
||||
switch coreId
|
||||
| C1 do icore = if(active) then 1 else 0
|
||||
| C2 do icore = if(active) then 2 else 0
|
||||
| C3 do icore = if(active) then 3 else 0
|
||||
| C4 do icore = if(active) then 4 else 0
|
||||
end;
|
||||
tel
|
||||
|
||||
|
||||
(* tells whether a task is running on core 3*)
|
||||
node comOn3(coreId:core)returns(yes:bool)
|
||||
let
|
||||
switch coreId
|
||||
| C1 do yes = false
|
||||
| C2 do yes = false
|
||||
| C3 do yes = true
|
||||
| C4 do yes = false
|
||||
end;
|
||||
tel
|
||||
|
||||
(* tells whether a task is running on core 1*)
|
||||
node comOn1(coreId:core)returns(yes:bool)
|
||||
let
|
||||
switch coreId
|
||||
| C1 do yes = true
|
||||
| C2 do yes = false
|
||||
| C3 do yes = false
|
||||
| C4 do yes = false
|
||||
end;
|
||||
tel
|
||||
|
||||
|
||||
(* tells whether two cores are equivalent *)
|
||||
node same_core(core1:core; core2: core) returns(samecore:bool)
|
||||
var sameproc:bool;
|
||||
task1_cpu, task1_core, task2_cpu, task2_core:bool;
|
||||
let
|
||||
switch core1
|
||||
| C1 do (task1_cpu, task1_core)=(false, false)
|
||||
| C2 do (task1_cpu, task1_core)=(false, true);
|
||||
| C3 do (task1_cpu, task1_core)=(true, false);
|
||||
| C4 do (task1_cpu, task1_core)=(true, true);
|
||||
end ;
|
||||
|
||||
switch core2
|
||||
| C1 do (task2_cpu, task2_core)=(false, false)
|
||||
| C2 do (task2_cpu, task2_core)=(false, true);
|
||||
| C3 do (task2_cpu, task2_core)=(true, false);
|
||||
| C4 do (task2_cpu, task2_core)=(true, true);
|
||||
end ;
|
||||
|
||||
sameproc = (task1_cpu & task2_cpu) or (not task1_cpu & not task2_cpu);
|
||||
samecore = sameproc & ((task1_core & task2_core) or (not task1_core & not task2_core));
|
||||
tel
|
||||
|
||||
|
||||
(* this implments the boolean equivalence *)
|
||||
|
||||
node bool_equi(a,b:bool) returns (res:bool)
|
||||
let
|
||||
res = ((a or not b) & (b or not a));
|
||||
tel
|
||||
|
||||
(* this implments the boolean implication *)
|
||||
|
||||
node bool_impl(a,b:bool) returns (res:bool)
|
||||
let
|
||||
res = (not a or b) ;
|
||||
tel
|
||||
|
||||
|
||||
|
||||
(* ==================================================================================*)
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
(* main program *)
|
||||
node main(disable: bool; fifoH1F, fifoH2F, fifoL2F, changeL2:bool; c_startH2_done, c_stopH2_done:bool) returns(
|
||||
h2Required:bool;
|
||||
h2NotRequired:bool;
|
||||
noOneOnC3WhenOff:bool;
|
||||
costgood:bool;
|
||||
notF2whenLogger:bool;
|
||||
startH2:bool; unboundH2:bool;
|
||||
startL2:bool; unboundL2:bool;
|
||||
c_startH2, c_stopH2, c_connectH2, c_diconnectH2:bool;
|
||||
c_startL, c_stopL, c_connectL, c_diconnectL:bool;
|
||||
a_cmd_pending:bool
|
||||
)
|
||||
|
||||
|
||||
|
||||
(* BEGIN CONTRACT *)
|
||||
(*====================================================*)
|
||||
contract
|
||||
|
||||
let
|
||||
|
||||
|
||||
tel
|
||||
assume(true)
|
||||
|
||||
enforce((a_cmd_pending or h2Required)
|
||||
& (a_cmd_pending or h2NotRequired)
|
||||
& noOneOnC3WhenOff
|
||||
& costgood
|
||||
& (a_cmd_pending or notF2whenLogger))
|
||||
with(cDa, cDb:bool;
|
||||
cSAa, cSAb:bool;
|
||||
cSBa, cSBb:bool;
|
||||
changeH2, killH2:bool
|
||||
)
|
||||
(*====================================================*)
|
||||
(* END CONTRACT *)
|
||||
|
||||
|
||||
var
|
||||
c_startH2_pending, c_stopH2_pending:bool;
|
||||
c1,c2,c3,c4:int; pf, pa, pd, pf1, pf2, pl:int;
|
||||
|
||||
(* these vars are true when no one is running on the associate core *)
|
||||
noOneOnC3:bool;
|
||||
|
||||
(* vars to describe the desired max corecosts
|
||||
when there is only 3 cores and when there is 4 cores available
|
||||
*)
|
||||
|
||||
costNActive:bool; costActive:bool;
|
||||
|
||||
(* component cores *)
|
||||
frend_core, ana_core, disp_core, file1_core, file2_core, logger_core :core;
|
||||
|
||||
|
||||
(* communication costs for each binding server/client side*)
|
||||
costAs, costAc:int; (*cost of the communication line between frend and ana*)
|
||||
costBs, costBc:int; (*cost of the communication line between ana and disp*)
|
||||
costCs, costCc:int; (*cost of the communication line between ana and logger*)
|
||||
costDs, costDc:int; (*cost of the communication line between disp and file1*)
|
||||
costFs, costFc:int; (*cost of the communication line between disp and file2*)
|
||||
|
||||
(*core 1,2,3,4 workload*)
|
||||
cost1, cost2, cost3, cost4: int;
|
||||
|
||||
costAs1, costAs2, costAs3, costAs4:int; (*cost of the communication line A on each core -- server side*)
|
||||
costBs1, costBs2, costBs3, costBs4:int; (*cost of the communication line B on each core -- server side*)
|
||||
costCs1, costCs2, costCs3, costCs4:int; (*cost of the communication line C on each core -- server side*)
|
||||
costDs1, costDs2, costDs3, costDs4:int; (*cost of the communication line D on each core -- server side*)
|
||||
costFs1, costFs2, costFs3, costFs4:int; (*cost of the communication line F on each core -- server side*)
|
||||
|
||||
costAc1, costAc2, costAc3, costAc4:int; (*cost of the communication line A on each core -- client side*)
|
||||
costBc1, costBc2, costBc3, costBc4:int; (*cost of the communication line B on each core -- client side*)
|
||||
costCc1, costCc2, costCc3, costCc4:int; (*cost of the communication line C on each core -- client side*)
|
||||
costDc1, costDc2, costDc3, costDc4:int; (*cost of the communication line D on each core -- client side*)
|
||||
costFc1, costFc2, costFc3, costFc4:int; (*cost of the communication line F on each core -- client side*)
|
||||
|
||||
core3:bool; (* state of the core number 3 ON/OFF*)
|
||||
|
||||
fifoH1Full, fifoH2Bull, fifoL2Bull : bool; (*satte of the fifos associated with filehandlers and logger*)
|
||||
|
||||
(* intermediate variables to control task positions *)
|
||||
iFa, iFb : bool;
|
||||
iAa, iAb : bool;
|
||||
iDa, iDb : bool;
|
||||
iF1a, iF1b : bool;
|
||||
iF2a, iF2b : bool;
|
||||
iLa, iLb : bool;
|
||||
|
||||
(* migration commands. those that are not output*)
|
||||
c_mig1f , c_mig2f , c_mig3f , c_mig4f,
|
||||
c_mig1a , c_mig2a , c_mig3a , c_mig4a,
|
||||
c_mig1f1 , c_mig2f1 , c_mig3f1 , c_mig4f1,
|
||||
c_mig1l , c_mig2l , c_mig3l , c_mig4l,
|
||||
c_mig1f2 , c_mig2f2 , c_mig3f2 , c_mig4f2 ,
|
||||
c_mig1d , c_mig2d , c_mig3d , c_mig4d:bool;
|
||||
|
||||
|
||||
(* two boolean variables to set the enforced propertie true for the 3 first instants *)
|
||||
count0, count1 : bool ;
|
||||
|
||||
let
|
||||
|
||||
|
||||
(* controlling task positions *)
|
||||
(iFa, iFb)=(false->true, false->true); (* frontend always on Core 2*)
|
||||
(iAa, iAb)=(false->true, false->true); (* analyzer manager always on Core2*)
|
||||
(iDa, iDb)=(true->cDa, false->cDb); (* dispa core 4 at the begining*)
|
||||
(iF1a, iF1b)=(true->cSAa, false->cSAb); (* fileh1 on core 4 at first *)
|
||||
(iF2a, iF2b)=(true->cSBa, false->cSBb); (* file2 core 4 at first *)
|
||||
(iLa, iLb)=(true->true, false->true); (* logger always on Core 4*)
|
||||
|
||||
|
||||
(* Computnig the cost of each core *)
|
||||
cost1= costAs1+ costBs1 + costCs1 + costDs1 + costFs1
|
||||
+ costAc1 + costBc1 + costCc1 + costDc1 + costFc1;
|
||||
|
||||
cost2= costAs2+ costBs2 + costCs2 + costDs2 + costFs2
|
||||
+ costAc2 + costBc2 + costCc2 + costDc2 + costFc2;
|
||||
|
||||
cost3= costAs3+ costBs3 + costCs3 + costDs3 + costFs3 +
|
||||
costAc3 + costBc3 + costCc3 + costDc3 + costFc3;
|
||||
|
||||
cost4= costAs4+ costBs4 + costCs4 + costDs4 + costFs4 +
|
||||
costAc4 + costBc4 + costCc4 + costDc4 + costFc4;
|
||||
|
||||
|
||||
|
||||
(* filehandler2 lifecycyle and the workload it induces *)
|
||||
(startH2, unboundH2, c_startH2, c_connectH2, c_stopH2, c_diconnectH2)= inlined lifecycle(not changeH2, not killH2 , not fifoH2Bull);
|
||||
(costFc, costFs) = if (not startH2) then (0,0) else inlined communication_cost(disp_core,file2_core);
|
||||
|
||||
|
||||
(* Logger lifeCycle and the workload it induces *)
|
||||
(startL2, unboundL2, c_startL, c_connectL, c_stopL, c_diconnectL)= inlined lifecycle(changeL2, false, not fifoL2Bull);
|
||||
(costCc, costCs) = if (not startL2) then (0,0) else inlined communication_cost(ana_core,logger_core);
|
||||
|
||||
|
||||
(*switch on/off core 3*)
|
||||
core3= inlined core_mode(disable);
|
||||
|
||||
|
||||
(* the fifio associated with file1 component input*)
|
||||
fifoH1Full = inlined fifo(fifoH1F);
|
||||
|
||||
(* the fifio associated with file2 component input*)
|
||||
fifoH2Bull = inlined fifo(fifoH2F);
|
||||
|
||||
(* the fifio associated with logger component input*)
|
||||
fifoL2Bull = inlined fifo(fifoL2F);
|
||||
|
||||
|
||||
(* component mapping *)
|
||||
(frend_core, c_mig1f , c_mig2f , c_mig3f , c_mig4f)= inlined position(iFa, iFb);
|
||||
(ana_core, c_mig1a , c_mig2a , c_mig3a , c_mig4a)= inlined position(iAa, iAb);
|
||||
(file1_core, c_mig1f1 , c_mig2f1 , c_mig3f1 , c_mig4f1)= inlined position(iF1a, iF1b);
|
||||
(disp_core, c_mig1d , c_mig2d , c_mig3d , c_mig4d)= inlined position(iDa, iDb);
|
||||
(file2_core, c_mig1f2 , c_mig2f2 , c_mig3f2 , c_mig4f2)= inlined position(iF2a, iF2b);
|
||||
(logger_core, c_mig1l , c_mig2l , c_mig3l , c_mig4l)= inlined position(iLa, iLb);
|
||||
|
||||
(* communication lines cost server/client side *)
|
||||
(costAc, costAs) = inlined communication_cost(frend_core, ana_core);
|
||||
(costBc, costBs) = inlined communication_cost(ana_core, disp_core);
|
||||
(costDc, costDs) = inlined communication_cost(disp_core, file1_core);
|
||||
|
||||
|
||||
|
||||
(* associating each communiaction line cost to the concerned processor *)
|
||||
(costAs1, costAs2, costAs3, costAs4) = inlined core_cost(ana_core, costAs);
|
||||
(costAc1, costAc2, costAc3, costAc4) = inlined core_cost(frend_core, costAc);
|
||||
|
||||
(costBs1, costBs2, costBs3, costBs4) = inlined core_cost(disp_core, costBs);
|
||||
(costBc1, costBc2, costBc3, costBc4) = inlined core_cost(ana_core, costBc);
|
||||
|
||||
(costCs1, costCs2, costCs3, costCs4) = inlined core_cost(logger_core, costCs);
|
||||
(costCc1, costCc2, costCc3, costCc4) = inlined core_cost(ana_core, costCc);
|
||||
|
||||
(costDs1, costDs2, costDs3, costDs4) = inlined core_cost(file1_core, costDs);
|
||||
(costDc1, costDc2, costDc3, costDc4) = inlined core_cost(disp_core, costDc);
|
||||
|
||||
(costFs1, costFs2, costFs3, costFs4) = inlined core_cost(file2_core, costFs);
|
||||
(costFc1, costFc2, costFc3, costFc4) = inlined core_cost(disp_core, costFc);
|
||||
|
||||
(* outputs/properties *)
|
||||
|
||||
(* core costs *)
|
||||
(c1, c2, c3, c4)= (cost1, cost2, cost3, cost4);
|
||||
|
||||
(* component positions -- from enumerated type to integers *)
|
||||
pf = inlined compute_core(frend_core, true);
|
||||
pa = inlined compute_core(ana_core, true);
|
||||
pf1 = inlined compute_core(file1_core, true);
|
||||
pf2 = inlined compute_core(file2_core, startH2);
|
||||
pl = inlined compute_core(logger_core, startL2);
|
||||
pd = inlined compute_core(disp_core, true);
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
noOneOnC3 = not (inlined comOn3(file1_core)
|
||||
or inlined comOn3(file2_core)
|
||||
or inlined comOn3(disp_core)
|
||||
or inlined comOn3(logger_core)
|
||||
or inlined comOn3(frend_core)
|
||||
or inlined comOn3(ana_core)
|
||||
);
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
count0 = false -> true;
|
||||
count1 = false fby count0;
|
||||
|
||||
|
||||
(* Asychronous commands *)
|
||||
c_startH2_pending= inlined command(c_startH2, c_startH2_done);
|
||||
c_stopH2_pending= inlined command(c_stopH2, c_stopH2_done);
|
||||
a_cmd_pending = c_startH2_pending or c_stopH2_pending;
|
||||
|
||||
(* properties to enforce *)
|
||||
|
||||
(* when logger is on, the file2 cannot be started *)
|
||||
notF2whenLogger = inlined bool_impl(startL2 & not unboundL2, unboundH2);
|
||||
|
||||
(*When core 3 is off, no one can run on it *) (*may be done without ifthenelse*)
|
||||
noOneOnC3WhenOff = if(core3) then true else noOneOnC3;
|
||||
|
||||
|
||||
(* FileHandler 2 is required when the fifo of file1 is full *)
|
||||
h2Required = inlined bool_impl(not startL2 & fifoH1Full, startH2 & not unboundH2);
|
||||
|
||||
(* FileHandler 2 is not required when the fifo of file1 is Empty *)
|
||||
(* We just disconnect it, it will be stopped once its fifo is empty*)
|
||||
h2NotRequired = inlined bool_impl(not fifoH1Full,unboundH2);
|
||||
|
||||
(* workload when 3 cores or 4 cores *)
|
||||
costActive=(c1<=170 & (c2<=180) & c3<=180 & c4<=140);
|
||||
costNActive=(c1<=280 & c2<=280 & c3<=280 & c4<=280);
|
||||
costgood = if(not count1)then true else (if core3 then costActive else costNActive);
|
||||
tel
|
||||
Loading…
Reference in New Issue