Introduction

Execution Chart

We display below the execution chart for this examination (boot time has been removed).

Sequence of Actions to be Executed by the VM

This is useful if one wants to reexecute the tool in the VM from the submitted image disk.

export BK_INPUT=LamportFastMutEx-PT-4
export BK_EXAMINATION=ReachabilityDeadlock
export BK_TOOL=cunf
export BK_RESULT_DIR=/tmp
export BK_LOG_FILE=/tmp/BenchKit_head_log_file.1718
export BIN_DIR=/home/mcc/BenchKit/bin
cd /home/mcc/BenchKit/INPUTS/LamportFastMutEx-PT-4
echo =====================================================================
echo ' Generated by BenchKit 1.0'
echo ' Executing tool cunf:'
echo ' Test is LamportFastMutEx-PT-4, examination is ReachabilityDeadlock'
echo =====================================================================
echo
echo --------------------
echo 'content from stdout:'
echo
bash /home/mcc/BenchKit/BenchKit_head.sh

Execution Outputs of cunf for LamportFastMutEx/4 (P/T)

This is useful if one wants to reexecute the tool in the VM from the submitted image disk.

execution on node 23: quadhexa-2.u-paris10.fr (runId=136955394400500_n_23)
=====================================================================
runnning cunf on LamportFastMutEx-PT-4 (ReachabilityDeadlock)
We got on stdout:
Probing ssh
Waiting ssh to respond
Ssh up and responding
=====================================================================
Generated by BenchKit 1.0
Executing tool cunf:
Test is LamportFastMutEx-PT-4, examination is ReachabilityDeadlock
=====================================================================

--------------------
content from stdout:

START 1371568823
FORMULA p_1_deadlock FALSE TECHNIQUES NET_UNFOLDING
CANNOT_COMPUTE
STOP 1371569241

--------------------
content from stderr:

bkh: PWD '/home/mcc/BenchKit/INPUTS/LamportFastMutEx-PT-4'
bkh: BK_EXAMINATION 'ReachabilityDeadlock'
bkh: iscolored FALSE
bkh: translating pnml to pep...
bkh: unfolding... cross the fingers to stay in memory!
bkh: yeah!
At size 14, 4096 histories
At size 15, 8192 histories
At size 17, 12288 histories
At size 18, 16384 histories
At size 18, 20480 histories
At size 19, 24576 histories
At size 20, 28672 histories
At size 21, 32768 histories
At size 22, 36864 histories
At size 22, 40960 histories
At size 23, 45056 histories
At size 24, 49152 histories
At size 24, 53248 histories
At size 25, 57344 histories
At size 26, 61440 histories
At size 26, 65536 histories
At size 27, 69632 histories
At size 27, 73728 histories
At size 28, 77824 histories
At size 28, 81920 histories
At size 29, 86016 histories
At size 29, 90112 histories
At size 29, 94208 histories
At size 30, 98304 histories
At size 30, 102400 histories
At size 30, 106496 histories
At size 31, 110592 histories
At size 31, 114688 histories
At size 31, 118784 histories
At size 32, 122880 histories
At size 32, 126976 histories
At size 33, 131072 histories
At size 33, 135168 histories
At size 33, 139264 histories
At size 34, 143360 histories
At size 34, 147456 histories
At size 35, 151552 histories
At size 35, 155648 histories
At size 36, 159744 histories
At size 36, 163840 histories
At size 37, 167936 histories
At size 38, 172032 histories
At size 38, 176128 histories
At size 39, 180224 histories
At size 39, 184320 histories
At size 40, 188416 histories
At size 41, 192512 histories
At size 42, 196608 histories
At size 42, 200704 histories
At size 43, 204800 histories
At size 44, 208896 histories
At size 45, 212992 histories
At size 46, 217088 histories
At size 48, 221184 histories
At size 49, 225280 histories
At size 51, 229376 histories
At size 53, 233472 histories
At size 55, 237568 histories
At size 58, 241664 histories
At size 62, 245760 histories
At size 69, 249856 histories
At size 92, 253952 histories
time 23.333
mem 351
hist 255933
events 75431
cond 113745
gen 282920
read 115962
comp 93298
r(h) 3.59
s(h) 0.49
co(r) 63.84
rco(r) 0.85
mrk(h) 14.00
pre(e) 1.55
ctx(e) 0.78
pst(e) 1.51
cutoffs 82932
ewhite 47482
egray 10884
eblack 17065
net /tmp/m.ll_net
main: Formula 0
deadlock: p.id().c_str()='p_1_deadlock'
inv_dead: p.id().c_str()='p_1_deadlock'
main: Formula 1
deadlock: p.id().c_str()='p_47_deadlock'
deadlock: Running cna: 'cna-mcc u.cuf /tmp/cna.out --deadlock --reduce 4-tree stb bin sccred'
debug: 0.0: load cuf
debug: 11.7: causal
debug: 15.9: sym
debug: 17.5: asym
debug: 294.7: dis
debug: 299.4: write cnf
debug: 358.1: solve
Traceback (most recent call last):
File "/home/mcc/BenchKit/bin//cna-mcc", line 13, in
sys.stderr ('cna: error: %s\n' % str (e))
TypeError: 'file' object is not callable
deadlock: buff=''

--------------------
content from /tmp/BenchKit_head_log_file.1718: