Skip to content
Snippets Groups Projects
Commit c33f25ab authored by Kristof's avatar Kristof
Browse files

- Introduced model of client clock as diff from server clock

- Experiments regarding performance
parent 521a0768
No related branches found
No related tags found
No related merge requests found
color 0a
TimeMem-1.0 verifyta -d ../Clocks-Test-4.xml Sanity-1.q >> Sanity-ALL-log.txt
\ No newline at end of file
TimeMem-1.0 verifyta -d ../Clocks-Test-6.xml Sanity-1.q >> Sanity-ALL-log.txt
\ No newline at end of file
color 0b
TimeMem-1.0 verifyta -b -S1 -C ../Clocks-Test-5.xml Sanity-2.q >> Sanity-2-log.txt
\ No newline at end of file
TimeMem-1.0 verifyta -b -S1 -C ../Clocks-Test-6.xml Sanity-2.q >> Sanity-2-log.txt
\ No newline at end of file
NEW RUN [1-15], Diff-int_range
:::
Options for the verification:
Generating no trace
Search order is breadth first
Using conservative space optimisation
Seed is 1466158213
Seed is 1467730671
State space representation uses difference bound matrices

Verifying property 1 at line 6
 -- Property is satisfied.
Exit code : 0
Elapsed time : 52.56
Kernel time : 0.22 (0.4%)
User time : 48.59 (92.5%)
page fault # : 34876
Working set : 135180 KB
Elapsed time : 202.27
Kernel time : 0.70 (0.3%)
User time : 193.30 (95.6%)
page fault # : 283748
Working set : 1086452 KB
Paged pool : 42 KB
Non-paged pool : 9 KB
Page file size : 144548 KB
Non-paged pool : 14 KB
Page file size : 1083288 KB
NEW RUN [1-15], Diff-dynamic_range
:::
Options for the verification:
Generating no trace
Search order is breadth first
Using conservative space optimisation
Seed is 1467731088
State space representation uses difference bound matrices

Verifying property 1 at line 6
 -- Property is satisfied.
Exit code : 0
Elapsed time : 43.34
Kernel time : 0.09 (0.2%)
User time : 43.23 (99.7%)
page fault # : 80584
Working set : 310808 KB
Paged pool : 42 KB
Non-paged pool : 10 KB
Page file size : 317020 KB
NEW RUN [1-15], Old
:::
Options for the verification:
Generating no trace
Search order is breadth first
Using conservative space optimisation
Seed is 1467731239
State space representation uses difference bound matrices

Verifying property 1 at line 6
 -- Property is satisfied.
Exit code : 0
Elapsed time : 64.98
Kernel time : 0.39 (0.6%)
User time : 64.15 (98.7%)
page fault # : 97728
Working set : 371192 KB
Paged pool : 42 KB
Non-paged pool : 10 KB
Page file size : 377604 KB
NEW RUN [2-7], Old
:::
Options for the verification:
Generating no trace
Search order is breadth first
Using conservative space optimisation
Seed is 1467731388
State space representation uses difference bound matrices

Verifying property 1 at line 6
 -- Property is NOT satisfied.
Exit code : 0
Elapsed time : 104.51
Kernel time : 0.22 (0.2%)
User time : 103.91 (99.4%)
page fault # : 135745
Working set : 519116 KB
Paged pool : 42 KB
Non-paged pool : 11 KB
Page file size : 523844 KB
NEW RUN [2-7], Diff-dynamic_range
:::
Options for the verification:
Generating no trace
Search order is breadth first
Using conservative space optimisation
Seed is 1467731544
State space representation uses difference bound matrices

Verifying property 1 at line 6
 -- Property is NOT satisfied.
Exit code : 0
Elapsed time : 80.79
Kernel time : 0.30 (0.4%)
User time : 79.83 (98.8%)
page fault # : 112003
Working set : 424180 KB
Paged pool : 42 KB
Non-paged pool : 10 KB
Page file size : 428948 KB
NEW RUN [3-7], Diff-dynamic_range
:::
Options for the verification:
Generating no trace
Search order is breadth first
Using conservative space optimisation
Seed is 1467731752
State space representation uses difference bound matrices

Verifying property 1 at line 6
 -- Aborted.
Out of memory.
\ No newline at end of file
color 0e
TimeMem-1.0 verifyta -b -S1 -C ../Clocks-Test-5.xml Sanity-3.q >> Sanity-3-log.txt
\ No newline at end of file
TimeMem-1.0 verifyta -b -S1 -C ../Clocks-Test-6.xml Sanity-3.q >> Sanity-3-log.txt
\ No newline at end of file
......@@ -3,4 +3,4 @@
/*
*/
A<> P_ClientBehavior.FINISH_PROCEDURE
\ No newline at end of file
A<> P_ClientBehavior.FINISH_PROCEDURE or P_ClientBehavior.FINISH_TIMEOUT
\ No newline at end of file
......@@ -58,12 +58,12 @@ E<> P_ClientBehavior.BROADCAST_FINISHED and (client_clock_counter - server_clock
/*
*/
E<> P_ClientBehavior.BROADCAST_FINISHED and (client_clock_counter - server_clock_counter <= -bc_interval_length) and (broadcast_repetitions_counter == 2)
E<> P_ClientBehavior.BROADCAST_FINISHED and (client_clock_counter() - server_clock_counter <= -bc_interval_length) and (broadcast_repetitions_counter == 2)
/*
*/
E<> P_ClientBehavior.BROADCAST_FINISHED and (client_clock_counter - server_clock_counter <= -bc_interval_length)
E<> P_ClientBehavior.BROADCAST_FINISHED and (client_clock_counter() - server_clock_counter <= -bc_interval_length)
/*
......
This diff is collapsed.
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment