Tue Jan 18 15:26:36 CET 2011 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/X01.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 X01 "PodWR" {} P0 ; MOV [y],$1 ; MOV EAX,[x] ; forall (0:EAX=0) Generated assembler _litmus_P0_0_: cmpl $0,%ecx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,(%rdi) _litmus_P0_4_: movl (%rbp),%eax _litmus_P0_5_: decl %ecx _litmus_P0_6_: Lit__L1: _litmus_P0_7_: jg Lit__L0 Test X01 Required Histogram (1 states) 1 :>0:EAX=0; Ok Witnesses Positive: 1, Negative: 0 Condition forall (0:EAX=0) is validated Hash=9aeb8cae8bcbf81616e760ef39d76121 Observation X01 Always 1 0 Time X01 0.08 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/X02.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 X02 "PodWR Fre PodWR Fre" {} P0 | P1 ; MOV [y],$1 | MOV [x],$1 ; MOV EAX,[x] | MOV EAX,[y] ; exists (0:EAX=0 /\ 1:EAX=0) Generated assembler _litmus_P1_0_: cmpl $0,%ecx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: movl $1,(%rbp) _litmus_P1_4_: movl (%rdi),%eax _litmus_P1_5_: decl %ecx _litmus_P1_6_: Lit__L3: _litmus_P1_7_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%ecx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,(%rdi) _litmus_P0_4_: movl (%rbp),%eax _litmus_P0_5_: decl %ecx _litmus_P0_6_: Lit__L1: _litmus_P0_7_: jg Lit__L0 Test X02 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0) is NOT validated Hash=eb447b2ffe44de821f49c40caa8e9757 Observation X02 Never 0 1 Time X02 0.39 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/X03.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 X03 "PodWR Fre PodWR Fre PodWR Fre" {} P0 | P1 | P2 ; MOV [z],$1 | MOV [x],$1 | MOV [y],$1 ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0) Generated assembler _litmus_P2_0_: cmpl $0,%edx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: movl $1,(%r9) _litmus_P2_4_: movl (%r8),%eax _litmus_P2_5_: decl %edx _litmus_P2_6_: Lit__L5: _litmus_P2_7_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%edx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: movl $1,(%r9) _litmus_P1_4_: movl (%r8),%eax _litmus_P1_5_: decl %edx _litmus_P1_6_: Lit__L3: _litmus_P1_7_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%edx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,(%r8) _litmus_P0_4_: movl (%r9),%eax _litmus_P0_5_: decl %edx _litmus_P0_6_: Lit__L1: _litmus_P0_7_: jg Lit__L0 Test X03 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0) is NOT validated Hash=7015574e5960da9548f7fd04ec792cdb Observation X03 Never 0 1 Time X03 0.29 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/X04.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 X04 "PodWR Fre PodWR Fre PodWR Fre PodWR Fre" {} P0 | P1 | P2 | P3 ; MOV [a],$1 | MOV [x],$1 | MOV [y],$1 | MOV [z],$1 ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] | MOV EAX,[a] ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0) Generated assembler _litmus_P3_0_: cmpl $0,%ecx _litmus_P3_1_: jmp Lit__L7 _litmus_P3_2_: Lit__L6: _litmus_P3_3_: movl $1,(%rdi) _litmus_P3_4_: movl (%rbp),%eax _litmus_P3_5_: decl %ecx _litmus_P3_6_: Lit__L7: _litmus_P3_7_: jg Lit__L6 _litmus_P2_0_: cmpl $0,%ecx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: movl $1,(%rbp) _litmus_P2_4_: movl (%rdi),%eax _litmus_P2_5_: decl %ecx _litmus_P2_6_: Lit__L5: _litmus_P2_7_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%ecx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: movl $1,(%rbp) _litmus_P1_4_: movl (%rdi),%eax _litmus_P1_5_: decl %ecx _litmus_P1_6_: Lit__L3: _litmus_P1_7_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%ecx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,(%rbp) _litmus_P0_4_: movl (%rdi),%eax _litmus_P0_5_: decl %ecx _litmus_P0_6_: Lit__L1: _litmus_P0_7_: jg Lit__L0 Test X04 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; 3:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0) is NOT validated Hash=4dbc449f6040a97331307a6f2e1561cc Observation X04 Never 0 1 Time X04 0.47 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/X05.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 X05 "PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre" {} P0 | P1 | P2 | P3 | P4 ; MOV [b],$1 | MOV [x],$1 | MOV [y],$1 | MOV [z],$1 | MOV [a],$1 ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] | MOV EAX,[a] | MOV EAX,[b] ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0) Generated assembler _litmus_P4_0_: cmpl $0,%edx _litmus_P4_1_: jmp Lit__L9 _litmus_P4_2_: Lit__L8: _litmus_P4_3_: movl $1,(%r9) _litmus_P4_4_: movl (%r8),%eax _litmus_P4_5_: decl %edx _litmus_P4_6_: Lit__L9: _litmus_P4_7_: jg Lit__L8 _litmus_P3_0_: cmpl $0,%edx _litmus_P3_1_: jmp Lit__L7 _litmus_P3_2_: Lit__L6: _litmus_P3_3_: movl $1,(%r8) _litmus_P3_4_: movl (%r9),%eax _litmus_P3_5_: decl %edx _litmus_P3_6_: Lit__L7: _litmus_P3_7_: jg Lit__L6 _litmus_P2_0_: cmpl $0,%edx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: movl $1,(%r9) _litmus_P2_4_: movl (%r8),%eax _litmus_P2_5_: decl %edx _litmus_P2_6_: Lit__L5: _litmus_P2_7_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%edx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: movl $1,(%r9) _litmus_P1_4_: movl (%r8),%eax _litmus_P1_5_: decl %edx _litmus_P1_6_: Lit__L3: _litmus_P1_7_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%edx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,(%r9) _litmus_P0_4_: movl (%r8),%eax _litmus_P0_5_: decl %edx _litmus_P0_6_: Lit__L1: _litmus_P0_7_: jg Lit__L0 Test X05 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; 3:EAX=1; 4:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0) is NOT validated Hash=3d5417305017c1a2164029a699c41244 Observation X05 Never 0 1 Time X05 0.40 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/X06.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 X06 "PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre" {} P0 | P1 | P2 | P3 | P4 | P5 ; MOV [c],$1 | MOV [x],$1 | MOV [y],$1 | MOV [z],$1 | MOV [a],$1 | MOV [b],$1 ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] | MOV EAX,[a] | MOV EAX,[b] | MOV EAX,[c] ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0) Generated assembler _litmus_P5_0_: cmpl $0,%edx _litmus_P5_1_: jmp Lit__L11 _litmus_P5_2_: Lit__L10: _litmus_P5_3_: movl $1,(%r9) _litmus_P5_4_: movl (%r8),%eax _litmus_P5_5_: decl %edx _litmus_P5_6_: Lit__L11: _litmus_P5_7_: jg Lit__L10 _litmus_P4_0_: cmpl $0,%edx _litmus_P4_1_: jmp Lit__L9 _litmus_P4_2_: Lit__L8: _litmus_P4_3_: movl $1,(%r9) _litmus_P4_4_: movl (%r8),%eax _litmus_P4_5_: decl %edx _litmus_P4_6_: Lit__L9: _litmus_P4_7_: jg Lit__L8 _litmus_P3_0_: cmpl $0,%edx _litmus_P3_1_: jmp Lit__L7 _litmus_P3_2_: Lit__L6: _litmus_P3_3_: movl $1,(%r8) _litmus_P3_4_: movl (%r9),%eax _litmus_P3_5_: decl %edx _litmus_P3_6_: Lit__L7: _litmus_P3_7_: jg Lit__L6 _litmus_P2_0_: cmpl $0,%edx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: movl $1,(%r9) _litmus_P2_4_: movl (%r8),%eax _litmus_P2_5_: decl %edx _litmus_P2_6_: Lit__L5: _litmus_P2_7_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%edx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: movl $1,(%r9) _litmus_P1_4_: movl (%r8),%eax _litmus_P1_5_: decl %edx _litmus_P1_6_: Lit__L3: _litmus_P1_7_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%edx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,(%r9) _litmus_P0_4_: movl (%r8),%eax _litmus_P0_5_: decl %edx _litmus_P0_6_: Lit__L1: _litmus_P0_7_: jg Lit__L0 Test X06 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; 3:EAX=1; 4:EAX=1; 5:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0) is NOT validated Hash=bf521f2563b67e83fcbf27497209ffff Observation X06 Never 0 1 Time X06 0.52 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/X07.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 X07 "PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre" {} P0 | P1 | P2 | P3 | P4 | P5 | P6 ; MOV [d],$1 | MOV [x],$1 | MOV [y],$1 | MOV [z],$1 | MOV [a],$1 | MOV [b],$1 | MOV [c],$1 ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] | MOV EAX,[a] | MOV EAX,[b] | MOV EAX,[c] | MOV EAX,[d] ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0 /\ 6:EAX=0) Generated assembler _litmus_P6_0_: cmpl $0,%edx _litmus_P6_1_: jmp Lit__L13 _litmus_P6_2_: Lit__L12: _litmus_P6_3_: movl $1,(%r9) _litmus_P6_4_: movl (%r8),%eax _litmus_P6_5_: decl %edx _litmus_P6_6_: Lit__L13: _litmus_P6_7_: jg Lit__L12 _litmus_P5_0_: cmpl $0,%edx _litmus_P5_1_: jmp Lit__L11 _litmus_P5_2_: Lit__L10: _litmus_P5_3_: movl $1,(%r9) _litmus_P5_4_: movl (%r8),%eax _litmus_P5_5_: decl %edx _litmus_P5_6_: Lit__L11: _litmus_P5_7_: jg Lit__L10 _litmus_P4_0_: cmpl $0,%edx _litmus_P4_1_: jmp Lit__L9 _litmus_P4_2_: Lit__L8: _litmus_P4_3_: movl $1,(%r9) _litmus_P4_4_: movl (%r8),%eax _litmus_P4_5_: decl %edx _litmus_P4_6_: Lit__L9: _litmus_P4_7_: jg Lit__L8 _litmus_P3_0_: cmpl $0,%edx _litmus_P3_1_: jmp Lit__L7 _litmus_P3_2_: Lit__L6: _litmus_P3_3_: movl $1,(%r8) _litmus_P3_4_: movl (%r9),%eax _litmus_P3_5_: decl %edx _litmus_P3_6_: Lit__L7: _litmus_P3_7_: jg Lit__L6 _litmus_P2_0_: cmpl $0,%edx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: movl $1,(%r9) _litmus_P2_4_: movl (%r8),%eax _litmus_P2_5_: decl %edx _litmus_P2_6_: Lit__L5: _litmus_P2_7_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%edx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: movl $1,(%r9) _litmus_P1_4_: movl (%r8),%eax _litmus_P1_5_: decl %edx _litmus_P1_6_: Lit__L3: _litmus_P1_7_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%edx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,(%r9) _litmus_P0_4_: movl (%r8),%eax _litmus_P0_5_: decl %edx _litmus_P0_6_: Lit__L1: _litmus_P0_7_: jg Lit__L0 Test X07 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; 3:EAX=1; 4:EAX=1; 5:EAX=1; 6:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0 /\ 6:EAX=0) is NOT validated Hash=82928d1f8482a5947c34cbde946c754a Observation X07 Never 0 1 Time X07 0.47 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/X08.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 X08 "PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre" {} P0 | P1 | P2 | P3 | P4 | P5 | P6 | P7 ; MOV [e],$1 | MOV [x],$1 | MOV [y],$1 | MOV [z],$1 | MOV [a],$1 | MOV [b],$1 | MOV [c],$1 | MOV [d],$1 ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] | MOV EAX,[a] | MOV EAX,[b] | MOV EAX,[c] | MOV EAX,[d] | MOV EAX,[e] ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0 /\ 6:EAX=0 /\ 7:EAX=0) Generated assembler _litmus_P7_0_: cmpl $0,%ecx _litmus_P7_1_: jmp Lit__L15 _litmus_P7_2_: Lit__L14: _litmus_P7_3_: movl $1,(%rbp) _litmus_P7_4_: movl (%rdi),%eax _litmus_P7_5_: decl %ecx _litmus_P7_6_: Lit__L15: _litmus_P7_7_: jg Lit__L14 _litmus_P6_0_: cmpl $0,%ecx _litmus_P6_1_: jmp Lit__L13 _litmus_P6_2_: Lit__L12: _litmus_P6_3_: movl $1,(%rbp) _litmus_P6_4_: movl (%rdi),%eax _litmus_P6_5_: decl %ecx _litmus_P6_6_: Lit__L13: _litmus_P6_7_: jg Lit__L12 _litmus_P5_0_: cmpl $0,%ecx _litmus_P5_1_: jmp Lit__L11 _litmus_P5_2_: Lit__L10: _litmus_P5_3_: movl $1,(%rbp) _litmus_P5_4_: movl (%rdi),%eax _litmus_P5_5_: decl %ecx _litmus_P5_6_: Lit__L11: _litmus_P5_7_: jg Lit__L10 _litmus_P4_0_: cmpl $0,%ecx _litmus_P4_1_: jmp Lit__L9 _litmus_P4_2_: Lit__L8: _litmus_P4_3_: movl $1,(%rbp) _litmus_P4_4_: movl (%rdi),%eax _litmus_P4_5_: decl %ecx _litmus_P4_6_: Lit__L9: _litmus_P4_7_: jg Lit__L8 _litmus_P3_0_: cmpl $0,%ecx _litmus_P3_1_: jmp Lit__L7 _litmus_P3_2_: Lit__L6: _litmus_P3_3_: movl $1,(%rdi) _litmus_P3_4_: movl (%rbp),%eax _litmus_P3_5_: decl %ecx _litmus_P3_6_: Lit__L7: _litmus_P3_7_: jg Lit__L6 _litmus_P2_0_: cmpl $0,%ecx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: movl $1,(%rbp) _litmus_P2_4_: movl (%rdi),%eax _litmus_P2_5_: decl %ecx _litmus_P2_6_: Lit__L5: _litmus_P2_7_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%ecx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: movl $1,(%rbp) _litmus_P1_4_: movl (%rdi),%eax _litmus_P1_5_: decl %ecx _litmus_P1_6_: Lit__L3: _litmus_P1_7_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%ecx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,(%rbp) _litmus_P0_4_: movl (%rdi),%eax _litmus_P0_5_: decl %ecx _litmus_P0_6_: Lit__L1: _litmus_P0_7_: jg Lit__L0 Test X08 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; 3:EAX=1; 4:EAX=1; 5:EAX=1; 6:EAX=1; 7:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0 /\ 6:EAX=0 /\ 7:EAX=0) is NOT validated Hash=8323e90886859c7004e205a9e3eefb84 Observation X08 Never 0 1 Time X08 0.59 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/F01.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 F01 "PodWR" {} P0 ; MOV [y],$1 ; MFENCE ; MOV EAX,[x] ; forall (0:EAX=0) Generated assembler _litmus_P0_0_: cmpl $0,%ecx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,(%rdi) _litmus_P0_4_: mfence _litmus_P0_5_: movl (%rbp),%eax _litmus_P0_6_: decl %ecx _litmus_P0_7_: Lit__L1: _litmus_P0_8_: jg Lit__L0 Test F01 Required Histogram (1 states) 1 :>0:EAX=0; Ok Witnesses Positive: 1, Negative: 0 Condition forall (0:EAX=0) is validated Hash=66ef0023d01159a20b9da833f0388a82 Observation F01 Always 1 0 Time F01 1.29 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/F02.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 F02 "MFencedWR Fre MFencedWR Fre" {} P0 | P1 ; MOV [y],$1 | MOV [x],$1 ; MFENCE | MFENCE ; MOV EAX,[x] | MOV EAX,[y] ; exists (0:EAX=0 /\ 1:EAX=0) Generated assembler _litmus_P1_0_: cmpl $0,%ecx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: movl $1,(%rbp) _litmus_P1_4_: mfence _litmus_P1_5_: movl (%rdi),%eax _litmus_P1_6_: decl %ecx _litmus_P1_7_: Lit__L3: _litmus_P1_8_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%ecx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,(%rdi) _litmus_P0_4_: mfence _litmus_P0_5_: movl (%rbp),%eax _litmus_P0_6_: decl %ecx _litmus_P0_7_: Lit__L1: _litmus_P0_8_: jg Lit__L0 Test F02 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0) is NOT validated Hash=60d067018c89f92ec3456c437f85c184 Observation F02 Never 0 1 Time F02 5.72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/F03.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 F03 "MFencedWR Fre MFencedWR Fre MFencedWR Fre" {} P0 | P1 | P2 ; MOV [z],$1 | MOV [x],$1 | MOV [y],$1 ; MFENCE | MFENCE | MFENCE ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0) Generated assembler _litmus_P2_0_: cmpl $0,%edx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: movl $1,(%r9) _litmus_P2_4_: mfence _litmus_P2_5_: movl (%r8),%eax _litmus_P2_6_: decl %edx _litmus_P2_7_: Lit__L5: _litmus_P2_8_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%edx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: movl $1,(%r9) _litmus_P1_4_: mfence _litmus_P1_5_: movl (%r8),%eax _litmus_P1_6_: decl %edx _litmus_P1_7_: Lit__L3: _litmus_P1_8_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%edx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,(%r8) _litmus_P0_4_: mfence _litmus_P0_5_: movl (%r9),%eax _litmus_P0_6_: decl %edx _litmus_P0_7_: Lit__L1: _litmus_P0_8_: jg Lit__L0 Test F03 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0) is NOT validated Hash=d766ec6d725495e398481f0ee334999d Observation F03 Never 0 1 Time F03 17.48 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/F04.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 F04 "MFencedWR Fre MFencedWR Fre MFencedWR Fre MFencedWR Fre" {} P0 | P1 | P2 | P3 ; MOV [a],$1 | MOV [x],$1 | MOV [y],$1 | MOV [z],$1 ; MFENCE | MFENCE | MFENCE | MFENCE ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] | MOV EAX,[a] ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0) Generated assembler _litmus_P3_0_: cmpl $0,%ecx _litmus_P3_1_: jmp Lit__L7 _litmus_P3_2_: Lit__L6: _litmus_P3_3_: movl $1,(%rdi) _litmus_P3_4_: mfence _litmus_P3_5_: movl (%rbp),%eax _litmus_P3_6_: decl %ecx _litmus_P3_7_: Lit__L7: _litmus_P3_8_: jg Lit__L6 _litmus_P2_0_: cmpl $0,%ecx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: movl $1,(%rbp) _litmus_P2_4_: mfence _litmus_P2_5_: movl (%rdi),%eax _litmus_P2_6_: decl %ecx _litmus_P2_7_: Lit__L5: _litmus_P2_8_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%ecx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: movl $1,(%rbp) _litmus_P1_4_: mfence _litmus_P1_5_: movl (%rdi),%eax _litmus_P1_6_: decl %ecx _litmus_P1_7_: Lit__L3: _litmus_P1_8_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%ecx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,(%rbp) _litmus_P0_4_: mfence _litmus_P0_5_: movl (%rdi),%eax _litmus_P0_6_: decl %ecx _litmus_P0_7_: Lit__L1: _litmus_P0_8_: jg Lit__L0 Test F04 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; 3:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0) is NOT validated Hash=695cf2c583c177e359c36b84e129a999 Observation F04 Never 0 1 Time F04 14.60 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/F05.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 F05 "MFencedWR Fre MFencedWR Fre MFencedWR Fre MFencedWR Fre MFencedWR Fre" {} P0 | P1 | P2 | P3 | P4 ; MOV [b],$1 | MOV [x],$1 | MOV [y],$1 | MOV [z],$1 | MOV [a],$1 ; MFENCE | MFENCE | MFENCE | MFENCE | MFENCE ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] | MOV EAX,[a] | MOV EAX,[b] ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0) Generated assembler _litmus_P4_0_: cmpl $0,%edx _litmus_P4_1_: jmp Lit__L9 _litmus_P4_2_: Lit__L8: _litmus_P4_3_: movl $1,(%r9) _litmus_P4_4_: mfence _litmus_P4_5_: movl (%r8),%eax _litmus_P4_6_: decl %edx _litmus_P4_7_: Lit__L9: _litmus_P4_8_: jg Lit__L8 _litmus_P3_0_: cmpl $0,%edx _litmus_P3_1_: jmp Lit__L7 _litmus_P3_2_: Lit__L6: _litmus_P3_3_: movl $1,(%r8) _litmus_P3_4_: mfence _litmus_P3_5_: movl (%r9),%eax _litmus_P3_6_: decl %edx _litmus_P3_7_: Lit__L7: _litmus_P3_8_: jg Lit__L6 _litmus_P2_0_: cmpl $0,%edx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: movl $1,(%r9) _litmus_P2_4_: mfence _litmus_P2_5_: movl (%r8),%eax _litmus_P2_6_: decl %edx _litmus_P2_7_: Lit__L5: _litmus_P2_8_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%edx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: movl $1,(%r9) _litmus_P1_4_: mfence _litmus_P1_5_: movl (%r8),%eax _litmus_P1_6_: decl %edx _litmus_P1_7_: Lit__L3: _litmus_P1_8_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%edx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,(%r9) _litmus_P0_4_: mfence _litmus_P0_5_: movl (%r8),%eax _litmus_P0_6_: decl %edx _litmus_P0_7_: Lit__L1: _litmus_P0_8_: jg Lit__L0 Test F05 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; 3:EAX=1; 4:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0) is NOT validated Hash=9fb09b401a6f60d80b37a5f79d1f82d2 Observation F05 Never 0 1 Time F05 17.44 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/F06.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 F06 "MFencedWR Fre MFencedWR Fre MFencedWR Fre MFencedWR Fre MFencedWR Fre MFencedWR Fre" {} P0 | P1 | P2 | P3 | P4 | P5 ; MOV [c],$1 | MOV [x],$1 | MOV [y],$1 | MOV [z],$1 | MOV [a],$1 | MOV [b],$1 ; MFENCE | MFENCE | MFENCE | MFENCE | MFENCE | MFENCE ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] | MOV EAX,[a] | MOV EAX,[b] | MOV EAX,[c] ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0) Generated assembler _litmus_P5_0_: cmpl $0,%edx _litmus_P5_1_: jmp Lit__L11 _litmus_P5_2_: Lit__L10: _litmus_P5_3_: movl $1,(%r9) _litmus_P5_4_: mfence _litmus_P5_5_: movl (%r8),%eax _litmus_P5_6_: decl %edx _litmus_P5_7_: Lit__L11: _litmus_P5_8_: jg Lit__L10 _litmus_P4_0_: cmpl $0,%edx _litmus_P4_1_: jmp Lit__L9 _litmus_P4_2_: Lit__L8: _litmus_P4_3_: movl $1,(%r9) _litmus_P4_4_: mfence _litmus_P4_5_: movl (%r8),%eax _litmus_P4_6_: decl %edx _litmus_P4_7_: Lit__L9: _litmus_P4_8_: jg Lit__L8 _litmus_P3_0_: cmpl $0,%edx _litmus_P3_1_: jmp Lit__L7 _litmus_P3_2_: Lit__L6: _litmus_P3_3_: movl $1,(%r8) _litmus_P3_4_: mfence _litmus_P3_5_: movl (%r9),%eax _litmus_P3_6_: decl %edx _litmus_P3_7_: Lit__L7: _litmus_P3_8_: jg Lit__L6 _litmus_P2_0_: cmpl $0,%edx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: movl $1,(%r9) _litmus_P2_4_: mfence _litmus_P2_5_: movl (%r8),%eax _litmus_P2_6_: decl %edx _litmus_P2_7_: Lit__L5: _litmus_P2_8_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%edx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: movl $1,(%r9) _litmus_P1_4_: mfence _litmus_P1_5_: movl (%r8),%eax _litmus_P1_6_: decl %edx _litmus_P1_7_: Lit__L3: _litmus_P1_8_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%edx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,(%r9) _litmus_P0_4_: mfence _litmus_P0_5_: movl (%r8),%eax _litmus_P0_6_: decl %edx _litmus_P0_7_: Lit__L1: _litmus_P0_8_: jg Lit__L0 Test F06 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; 3:EAX=1; 4:EAX=1; 5:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0) is NOT validated Hash=baed0d428e5d54320f7b33eac7b76177 Observation F06 Never 0 1 Time F06 17.04 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/F07.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 F07 "MFencedWR Fre MFencedWR Fre MFencedWR Fre MFencedWR Fre MFencedWR Fre MFencedWR Fre MFencedWR Fre" {} P0 | P1 | P2 | P3 | P4 | P5 | P6 ; MOV [d],$1 | MOV [x],$1 | MOV [y],$1 | MOV [z],$1 | MOV [a],$1 | MOV [b],$1 | MOV [c],$1 ; MFENCE | MFENCE | MFENCE | MFENCE | MFENCE | MFENCE | MFENCE ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] | MOV EAX,[a] | MOV EAX,[b] | MOV EAX,[c] | MOV EAX,[d] ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0 /\ 6:EAX=0) Generated assembler _litmus_P6_0_: cmpl $0,%edx _litmus_P6_1_: jmp Lit__L13 _litmus_P6_2_: Lit__L12: _litmus_P6_3_: movl $1,(%r9) _litmus_P6_4_: mfence _litmus_P6_5_: movl (%r8),%eax _litmus_P6_6_: decl %edx _litmus_P6_7_: Lit__L13: _litmus_P6_8_: jg Lit__L12 _litmus_P5_0_: cmpl $0,%edx _litmus_P5_1_: jmp Lit__L11 _litmus_P5_2_: Lit__L10: _litmus_P5_3_: movl $1,(%r9) _litmus_P5_4_: mfence _litmus_P5_5_: movl (%r8),%eax _litmus_P5_6_: decl %edx _litmus_P5_7_: Lit__L11: _litmus_P5_8_: jg Lit__L10 _litmus_P4_0_: cmpl $0,%edx _litmus_P4_1_: jmp Lit__L9 _litmus_P4_2_: Lit__L8: _litmus_P4_3_: movl $1,(%r9) _litmus_P4_4_: mfence _litmus_P4_5_: movl (%r8),%eax _litmus_P4_6_: decl %edx _litmus_P4_7_: Lit__L9: _litmus_P4_8_: jg Lit__L8 _litmus_P3_0_: cmpl $0,%edx _litmus_P3_1_: jmp Lit__L7 _litmus_P3_2_: Lit__L6: _litmus_P3_3_: movl $1,(%r8) _litmus_P3_4_: mfence _litmus_P3_5_: movl (%r9),%eax _litmus_P3_6_: decl %edx _litmus_P3_7_: Lit__L7: _litmus_P3_8_: jg Lit__L6 _litmus_P2_0_: cmpl $0,%edx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: movl $1,(%r9) _litmus_P2_4_: mfence _litmus_P2_5_: movl (%r8),%eax _litmus_P2_6_: decl %edx _litmus_P2_7_: Lit__L5: _litmus_P2_8_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%edx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: movl $1,(%r9) _litmus_P1_4_: mfence _litmus_P1_5_: movl (%r8),%eax _litmus_P1_6_: decl %edx _litmus_P1_7_: Lit__L3: _litmus_P1_8_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%edx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,(%r9) _litmus_P0_4_: mfence _litmus_P0_5_: movl (%r8),%eax _litmus_P0_6_: decl %edx _litmus_P0_7_: Lit__L1: _litmus_P0_8_: jg Lit__L0 Test F07 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; 3:EAX=1; 4:EAX=1; 5:EAX=1; 6:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0 /\ 6:EAX=0) is NOT validated Hash=b728efd04bb25780741d096d58b2b1a6 Observation F07 Never 0 1 Time F07 16.90 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/F08.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 F08 "MFencedWR Fre MFencedWR Fre MFencedWR Fre MFencedWR Fre MFencedWR Fre MFencedWR Fre MFencedWR Fre MFencedWR Fre" {} P0 | P1 | P2 | P3 | P4 | P5 | P6 | P7 ; MOV [e],$1 | MOV [x],$1 | MOV [y],$1 | MOV [z],$1 | MOV [a],$1 | MOV [b],$1 | MOV [c],$1 | MOV [d],$1 ; MFENCE | MFENCE | MFENCE | MFENCE | MFENCE | MFENCE | MFENCE | MFENCE ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] | MOV EAX,[a] | MOV EAX,[b] | MOV EAX,[c] | MOV EAX,[d] | MOV EAX,[e] ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0 /\ 6:EAX=0 /\ 7:EAX=0) Generated assembler _litmus_P7_0_: cmpl $0,%ecx _litmus_P7_1_: jmp Lit__L15 _litmus_P7_2_: Lit__L14: _litmus_P7_3_: movl $1,(%rbp) _litmus_P7_4_: mfence _litmus_P7_5_: movl (%rdi),%eax _litmus_P7_6_: decl %ecx _litmus_P7_7_: Lit__L15: _litmus_P7_8_: jg Lit__L14 _litmus_P6_0_: cmpl $0,%ecx _litmus_P6_1_: jmp Lit__L13 _litmus_P6_2_: Lit__L12: _litmus_P6_3_: movl $1,(%rbp) _litmus_P6_4_: mfence _litmus_P6_5_: movl (%rdi),%eax _litmus_P6_6_: decl %ecx _litmus_P6_7_: Lit__L13: _litmus_P6_8_: jg Lit__L12 _litmus_P5_0_: cmpl $0,%ecx _litmus_P5_1_: jmp Lit__L11 _litmus_P5_2_: Lit__L10: _litmus_P5_3_: movl $1,(%rbp) _litmus_P5_4_: mfence _litmus_P5_5_: movl (%rdi),%eax _litmus_P5_6_: decl %ecx _litmus_P5_7_: Lit__L11: _litmus_P5_8_: jg Lit__L10 _litmus_P4_0_: cmpl $0,%ecx _litmus_P4_1_: jmp Lit__L9 _litmus_P4_2_: Lit__L8: _litmus_P4_3_: movl $1,(%rbp) _litmus_P4_4_: mfence _litmus_P4_5_: movl (%rdi),%eax _litmus_P4_6_: decl %ecx _litmus_P4_7_: Lit__L9: _litmus_P4_8_: jg Lit__L8 _litmus_P3_0_: cmpl $0,%ecx _litmus_P3_1_: jmp Lit__L7 _litmus_P3_2_: Lit__L6: _litmus_P3_3_: movl $1,(%rdi) _litmus_P3_4_: mfence _litmus_P3_5_: movl (%rbp),%eax _litmus_P3_6_: decl %ecx _litmus_P3_7_: Lit__L7: _litmus_P3_8_: jg Lit__L6 _litmus_P2_0_: cmpl $0,%ecx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: movl $1,(%rbp) _litmus_P2_4_: mfence _litmus_P2_5_: movl (%rdi),%eax _litmus_P2_6_: decl %ecx _litmus_P2_7_: Lit__L5: _litmus_P2_8_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%ecx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: movl $1,(%rbp) _litmus_P1_4_: mfence _litmus_P1_5_: movl (%rdi),%eax _litmus_P1_6_: decl %ecx _litmus_P1_7_: Lit__L3: _litmus_P1_8_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%ecx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,(%rbp) _litmus_P0_4_: mfence _litmus_P0_5_: movl (%rdi),%eax _litmus_P0_6_: decl %ecx _litmus_P0_7_: Lit__L1: _litmus_P0_8_: jg Lit__L0 Test F08 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; 3:EAX=1; 4:EAX=1; 5:EAX=1; 6:EAX=1; 7:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0 /\ 6:EAX=0 /\ 7:EAX=0) is NOT validated Hash=b806667ff558839c7b761cf0442d8e58 Observation F08 Never 0 1 Time F08 16.56 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/A01.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 A01 "PodWR" {} P0 ; MOV EBX,$1 ; XCHG [y],EBX ; MOV EAX,[x] ; forall (0:EAX=0) Generated assembler _litmus_P0_0_: cmpl $0,%edx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,%r11d _litmus_P0_4_: xchgl %r11d,(%rdi) _litmus_P0_5_: movl (%rbp),%eax _litmus_P0_6_: decl %edx _litmus_P0_7_: Lit__L1: _litmus_P0_8_: jg Lit__L0 Test A01 Required Histogram (1 states) 1 :>0:EAX=0; Ok Witnesses Positive: 1, Negative: 0 Condition forall (0:EAX=0) is validated Hash=03f809bce2f2e672e456d1f06da7e3fb Observation A01 Always 1 0 Time A01 0.72 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/A02.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 A02 "PodWR Fre PodWR Fre" {} P0 | P1 ; MOV EBX,$1 | MOV EBX,$1 ; XCHG [y],EBX | XCHG [x],EBX ; MOV EAX,[x] | MOV EAX,[y] ; exists (0:EAX=0 /\ 1:EAX=0) Generated assembler _litmus_P1_0_: cmpl $0,%ecx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: movl $1,%r10d _litmus_P1_4_: xchgl %r10d,(%rbp) _litmus_P1_5_: movl (%rdi),%eax _litmus_P1_6_: decl %ecx _litmus_P1_7_: Lit__L3: _litmus_P1_8_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%ecx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,%r10d _litmus_P0_4_: xchgl %r10d,(%rdi) _litmus_P0_5_: movl (%rbp),%eax _litmus_P0_6_: decl %ecx _litmus_P0_7_: Lit__L1: _litmus_P0_8_: jg Lit__L0 Test A02 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0) is NOT validated Hash=9663769e0c2741a1aa8145f9b9ce5ecb Observation A02 Never 0 1 Time A02 5.24 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/A03.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 A03 "PodWR Fre PodWR Fre PodWR Fre" {} P0 | P1 | P2 ; MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 ; XCHG [z],EBX | XCHG [x],EBX | XCHG [y],EBX ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0) Generated assembler _litmus_P2_0_: cmpl $0,%edx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: movl $1,%ebp _litmus_P2_4_: xchgl %ebp,(%r9) _litmus_P2_5_: movl (%r8),%eax _litmus_P2_6_: decl %edx _litmus_P2_7_: Lit__L5: _litmus_P2_8_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%edx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: movl $1,%ebp _litmus_P1_4_: xchgl %ebp,(%r9) _litmus_P1_5_: movl (%r8),%eax _litmus_P1_6_: decl %edx _litmus_P1_7_: Lit__L3: _litmus_P1_8_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%edx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,%ebp _litmus_P0_4_: xchgl %ebp,(%r8) _litmus_P0_5_: movl (%r9),%eax _litmus_P0_6_: decl %edx _litmus_P0_7_: Lit__L1: _litmus_P0_8_: jg Lit__L0 Test A03 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0) is NOT validated Hash=896026d247b917eddc04f54a02273d38 Observation A03 Never 0 1 Time A03 10.81 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/A04.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 A04 "PodWR Fre PodWR Fre PodWR Fre PodWR Fre" {} P0 | P1 | P2 | P3 ; MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 ; XCHG [a],EBX | XCHG [x],EBX | XCHG [y],EBX | XCHG [z],EBX ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] | MOV EAX,[a] ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0) Generated assembler _litmus_P3_0_: cmpl $0,%ecx _litmus_P3_1_: jmp Lit__L7 _litmus_P3_2_: Lit__L6: _litmus_P3_3_: movl $1,%r10d _litmus_P3_4_: xchgl %r10d,(%rdi) _litmus_P3_5_: movl (%rbp),%eax _litmus_P3_6_: decl %ecx _litmus_P3_7_: Lit__L7: _litmus_P3_8_: jg Lit__L6 _litmus_P2_0_: cmpl $0,%ecx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: movl $1,%r10d _litmus_P2_4_: xchgl %r10d,(%rbp) _litmus_P2_5_: movl (%rdi),%eax _litmus_P2_6_: decl %ecx _litmus_P2_7_: Lit__L5: _litmus_P2_8_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%ecx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: movl $1,%r10d _litmus_P1_4_: xchgl %r10d,(%rbp) _litmus_P1_5_: movl (%rdi),%eax _litmus_P1_6_: decl %ecx _litmus_P1_7_: Lit__L3: _litmus_P1_8_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%ecx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,%r10d _litmus_P0_4_: xchgl %r10d,(%rbp) _litmus_P0_5_: movl (%rdi),%eax _litmus_P0_6_: decl %ecx _litmus_P0_7_: Lit__L1: _litmus_P0_8_: jg Lit__L0 Test A04 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; 3:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0) is NOT validated Hash=9d8f2889d7e8e3ddbe5384a3e93f011d Observation A04 Never 0 1 Time A04 14.26 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/A05.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 A05 "PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre" {} P0 | P1 | P2 | P3 | P4 ; MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 ; XCHG [b],EBX | XCHG [x],EBX | XCHG [y],EBX | XCHG [z],EBX | XCHG [a],EBX ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] | MOV EAX,[a] | MOV EAX,[b] ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0) Generated assembler _litmus_P4_0_: cmpl $0,%edx _litmus_P4_1_: jmp Lit__L9 _litmus_P4_2_: Lit__L8: _litmus_P4_3_: movl $1,%ebp _litmus_P4_4_: xchgl %ebp,(%r9) _litmus_P4_5_: movl (%r8),%eax _litmus_P4_6_: decl %edx _litmus_P4_7_: Lit__L9: _litmus_P4_8_: jg Lit__L8 _litmus_P3_0_: cmpl $0,%edx _litmus_P3_1_: jmp Lit__L7 _litmus_P3_2_: Lit__L6: _litmus_P3_3_: movl $1,%ebp _litmus_P3_4_: xchgl %ebp,(%r8) _litmus_P3_5_: movl (%r9),%eax _litmus_P3_6_: decl %edx _litmus_P3_7_: Lit__L7: _litmus_P3_8_: jg Lit__L6 _litmus_P2_0_: cmpl $0,%edx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: movl $1,%ebp _litmus_P2_4_: xchgl %ebp,(%r9) _litmus_P2_5_: movl (%r8),%eax _litmus_P2_6_: decl %edx _litmus_P2_7_: Lit__L5: _litmus_P2_8_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%edx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: movl $1,%ebp _litmus_P1_4_: xchgl %ebp,(%r9) _litmus_P1_5_: movl (%r8),%eax _litmus_P1_6_: decl %edx _litmus_P1_7_: Lit__L3: _litmus_P1_8_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%edx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,%ebp _litmus_P0_4_: xchgl %ebp,(%r9) _litmus_P0_5_: movl (%r8),%eax _litmus_P0_6_: decl %edx _litmus_P0_7_: Lit__L1: _litmus_P0_8_: jg Lit__L0 Test A05 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; 3:EAX=1; 4:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0) is NOT validated Hash=e3d36619a6eb4a10314070b43ed03d33 Observation A05 Never 0 1 Time A05 18.64 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/A06.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 A06 "PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre" {} P0 | P1 | P2 | P3 | P4 | P5 ; MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 ; XCHG [c],EBX | XCHG [x],EBX | XCHG [y],EBX | XCHG [z],EBX | XCHG [a],EBX | XCHG [b],EBX ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] | MOV EAX,[a] | MOV EAX,[b] | MOV EAX,[c] ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0) Generated assembler _litmus_P5_0_: cmpl $0,%edx _litmus_P5_1_: jmp Lit__L11 _litmus_P5_2_: Lit__L10: _litmus_P5_3_: movl $1,%ebp _litmus_P5_4_: xchgl %ebp,(%r9) _litmus_P5_5_: movl (%r8),%eax _litmus_P5_6_: decl %edx _litmus_P5_7_: Lit__L11: _litmus_P5_8_: jg Lit__L10 _litmus_P4_0_: cmpl $0,%edx _litmus_P4_1_: jmp Lit__L9 _litmus_P4_2_: Lit__L8: _litmus_P4_3_: movl $1,%ebp _litmus_P4_4_: xchgl %ebp,(%r9) _litmus_P4_5_: movl (%r8),%eax _litmus_P4_6_: decl %edx _litmus_P4_7_: Lit__L9: _litmus_P4_8_: jg Lit__L8 _litmus_P3_0_: cmpl $0,%edx _litmus_P3_1_: jmp Lit__L7 _litmus_P3_2_: Lit__L6: _litmus_P3_3_: movl $1,%ebp _litmus_P3_4_: xchgl %ebp,(%r8) _litmus_P3_5_: movl (%r9),%eax _litmus_P3_6_: decl %edx _litmus_P3_7_: Lit__L7: _litmus_P3_8_: jg Lit__L6 _litmus_P2_0_: cmpl $0,%edx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: movl $1,%ebp _litmus_P2_4_: xchgl %ebp,(%r9) _litmus_P2_5_: movl (%r8),%eax _litmus_P2_6_: decl %edx _litmus_P2_7_: Lit__L5: _litmus_P2_8_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%edx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: movl $1,%ebp _litmus_P1_4_: xchgl %ebp,(%r9) _litmus_P1_5_: movl (%r8),%eax _litmus_P1_6_: decl %edx _litmus_P1_7_: Lit__L3: _litmus_P1_8_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%edx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,%ebp _litmus_P0_4_: xchgl %ebp,(%r9) _litmus_P0_5_: movl (%r8),%eax _litmus_P0_6_: decl %edx _litmus_P0_7_: Lit__L1: _litmus_P0_8_: jg Lit__L0 Test A06 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; 3:EAX=1; 4:EAX=1; 5:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0) is NOT validated Hash=dc03aebbfcc14a1bc010465c83bb42bf Observation A06 Never 0 1 Time A06 13.16 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/A07.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 A07 "PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre" {} P0 | P1 | P2 | P3 | P4 | P5 | P6 ; MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 ; XCHG [d],EBX | XCHG [x],EBX | XCHG [y],EBX | XCHG [z],EBX | XCHG [a],EBX | XCHG [b],EBX | XCHG [c],EBX ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] | MOV EAX,[a] | MOV EAX,[b] | MOV EAX,[c] | MOV EAX,[d] ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0 /\ 6:EAX=0) Generated assembler _litmus_P6_0_: cmpl $0,%edx _litmus_P6_1_: jmp Lit__L13 _litmus_P6_2_: Lit__L12: _litmus_P6_3_: movl $1,%ebp _litmus_P6_4_: xchgl %ebp,(%r9) _litmus_P6_5_: movl (%r8),%eax _litmus_P6_6_: decl %edx _litmus_P6_7_: Lit__L13: _litmus_P6_8_: jg Lit__L12 _litmus_P5_0_: cmpl $0,%edx _litmus_P5_1_: jmp Lit__L11 _litmus_P5_2_: Lit__L10: _litmus_P5_3_: movl $1,%ebp _litmus_P5_4_: xchgl %ebp,(%r9) _litmus_P5_5_: movl (%r8),%eax _litmus_P5_6_: decl %edx _litmus_P5_7_: Lit__L11: _litmus_P5_8_: jg Lit__L10 _litmus_P4_0_: cmpl $0,%edx _litmus_P4_1_: jmp Lit__L9 _litmus_P4_2_: Lit__L8: _litmus_P4_3_: movl $1,%ebp _litmus_P4_4_: xchgl %ebp,(%r9) _litmus_P4_5_: movl (%r8),%eax _litmus_P4_6_: decl %edx _litmus_P4_7_: Lit__L9: _litmus_P4_8_: jg Lit__L8 _litmus_P3_0_: cmpl $0,%edx _litmus_P3_1_: jmp Lit__L7 _litmus_P3_2_: Lit__L6: _litmus_P3_3_: movl $1,%ebp _litmus_P3_4_: xchgl %ebp,(%r8) _litmus_P3_5_: movl (%r9),%eax _litmus_P3_6_: decl %edx _litmus_P3_7_: Lit__L7: _litmus_P3_8_: jg Lit__L6 _litmus_P2_0_: cmpl $0,%edx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: movl $1,%ebp _litmus_P2_4_: xchgl %ebp,(%r9) _litmus_P2_5_: movl (%r8),%eax _litmus_P2_6_: decl %edx _litmus_P2_7_: Lit__L5: _litmus_P2_8_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%edx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: movl $1,%ebp _litmus_P1_4_: xchgl %ebp,(%r9) _litmus_P1_5_: movl (%r8),%eax _litmus_P1_6_: decl %edx _litmus_P1_7_: Lit__L3: _litmus_P1_8_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%edx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,%ebp _litmus_P0_4_: xchgl %ebp,(%r9) _litmus_P0_5_: movl (%r8),%eax _litmus_P0_6_: decl %edx _litmus_P0_7_: Lit__L1: _litmus_P0_8_: jg Lit__L0 Test A07 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; 3:EAX=1; 4:EAX=1; 5:EAX=1; 6:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0 /\ 6:EAX=0) is NOT validated Hash=f02947ccb34b45be45cf05db19dded8b Observation A07 Never 0 1 Time A07 16.02 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/A08.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 A08 "PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre" {} P0 | P1 | P2 | P3 | P4 | P5 | P6 | P7 ; MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 ; XCHG [e],EBX | XCHG [x],EBX | XCHG [y],EBX | XCHG [z],EBX | XCHG [a],EBX | XCHG [b],EBX | XCHG [c],EBX | XCHG [d],EBX ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] | MOV EAX,[a] | MOV EAX,[b] | MOV EAX,[c] | MOV EAX,[d] | MOV EAX,[e] ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0 /\ 6:EAX=0 /\ 7:EAX=0) Generated assembler _litmus_P7_0_: cmpl $0,%ecx _litmus_P7_1_: jmp Lit__L15 _litmus_P7_2_: Lit__L14: _litmus_P7_3_: movl $1,%r10d _litmus_P7_4_: xchgl %r10d,(%rbp) _litmus_P7_5_: movl (%rdi),%eax _litmus_P7_6_: decl %ecx _litmus_P7_7_: Lit__L15: _litmus_P7_8_: jg Lit__L14 _litmus_P6_0_: cmpl $0,%ecx _litmus_P6_1_: jmp Lit__L13 _litmus_P6_2_: Lit__L12: _litmus_P6_3_: movl $1,%r10d _litmus_P6_4_: xchgl %r10d,(%rbp) _litmus_P6_5_: movl (%rdi),%eax _litmus_P6_6_: decl %ecx _litmus_P6_7_: Lit__L13: _litmus_P6_8_: jg Lit__L12 _litmus_P5_0_: cmpl $0,%ecx _litmus_P5_1_: jmp Lit__L11 _litmus_P5_2_: Lit__L10: _litmus_P5_3_: movl $1,%r10d _litmus_P5_4_: xchgl %r10d,(%rbp) _litmus_P5_5_: movl (%rdi),%eax _litmus_P5_6_: decl %ecx _litmus_P5_7_: Lit__L11: _litmus_P5_8_: jg Lit__L10 _litmus_P4_0_: cmpl $0,%ecx _litmus_P4_1_: jmp Lit__L9 _litmus_P4_2_: Lit__L8: _litmus_P4_3_: movl $1,%r10d _litmus_P4_4_: xchgl %r10d,(%rbp) _litmus_P4_5_: movl (%rdi),%eax _litmus_P4_6_: decl %ecx _litmus_P4_7_: Lit__L9: _litmus_P4_8_: jg Lit__L8 _litmus_P3_0_: cmpl $0,%ecx _litmus_P3_1_: jmp Lit__L7 _litmus_P3_2_: Lit__L6: _litmus_P3_3_: movl $1,%r10d _litmus_P3_4_: xchgl %r10d,(%rdi) _litmus_P3_5_: movl (%rbp),%eax _litmus_P3_6_: decl %ecx _litmus_P3_7_: Lit__L7: _litmus_P3_8_: jg Lit__L6 _litmus_P2_0_: cmpl $0,%ecx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: movl $1,%r10d _litmus_P2_4_: xchgl %r10d,(%rbp) _litmus_P2_5_: movl (%rdi),%eax _litmus_P2_6_: decl %ecx _litmus_P2_7_: Lit__L5: _litmus_P2_8_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%ecx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: movl $1,%r10d _litmus_P1_4_: xchgl %r10d,(%rbp) _litmus_P1_5_: movl (%rdi),%eax _litmus_P1_6_: decl %ecx _litmus_P1_7_: Lit__L3: _litmus_P1_8_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%ecx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: movl $1,%r10d _litmus_P0_4_: xchgl %r10d,(%rbp) _litmus_P0_5_: movl (%rdi),%eax _litmus_P0_6_: decl %ecx _litmus_P0_7_: Lit__L1: _litmus_P0_8_: jg Lit__L0 Test A08 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; 3:EAX=1; 4:EAX=1; 5:EAX=1; 6:EAX=1; 7:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0 /\ 6:EAX=0 /\ 7:EAX=0) is NOT validated Hash=2ed0cadcb26cdafcbfb31823a7c68889 Observation A08 Never 0 1 Time A08 12.29 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/L01.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 L01 "PodWR" {} P0 ; Lock00: ; MOV EBX,$1 ; XCHG [L_y],EBX ; CMP EBX,$0 ; JE Lock02 ; Lock01: ; MOV EBX,[L_y] ; CMP EBX,$0 ; JE Lock00 ; JMP Lock01 ; Lock02: ; MOV [y],$1 ; MOV [L_y],$0 ; Lock03: ; MOV EBX,$1 ; XCHG [L_x],EBX ; CMP EBX,$0 ; JE Lock05 ; Lock04: ; MOV EBX,[L_x] ; CMP EBX,$0 ; JE Lock03 ; JMP Lock04 ; Lock05: ; MOV EAX,[x] ; MOV [L_x],$0 ; forall (0:EAX=0) Generated assembler _litmus_P0_0_: cmpl $0,%edx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: LitLock00: _litmus_P0_4_: movl $1,%r13d _litmus_P0_5_: xchgl %r13d,(%r8) _litmus_P0_6_: cmpl $0,%r13d _litmus_P0_7_: je LitLock02 _litmus_P0_8_: LitLock01: _litmus_P0_9_: movl (%r8),%r13d _litmus_P0_10_: cmpl $0,%r13d _litmus_P0_11_: je LitLock00 _litmus_P0_12_: jmp LitLock01 _litmus_P0_13_: LitLock02: _litmus_P0_14_: movl $1,(%rdi) _litmus_P0_15_: movl $0,(%r8) _litmus_P0_16_: LitLock03: _litmus_P0_17_: movl $1,%r13d _litmus_P0_18_: xchgl %r13d,(%r9) _litmus_P0_19_: cmpl $0,%r13d _litmus_P0_20_: je LitLock05 _litmus_P0_21_: LitLock04: _litmus_P0_22_: movl (%r9),%r13d _litmus_P0_23_: cmpl $0,%r13d _litmus_P0_24_: je LitLock03 _litmus_P0_25_: jmp LitLock04 _litmus_P0_26_: LitLock05: _litmus_P0_27_: movl (%rbp),%eax _litmus_P0_28_: movl $0,(%r9) _litmus_P0_29_: decl %edx _litmus_P0_30_: Lit__L1: _litmus_P0_31_: jg Lit__L0 Test L01 Required Histogram (1 states) 1 :>0:EAX=0; Ok Witnesses Positive: 1, Negative: 0 Condition forall (0:EAX=0) is validated Hash=f2685d58ed3fecaa7dc27e2cc00d3038 Observation L01 Always 1 0 Time L01 1.86 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/L02.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 L02 "PodWR Fre PodWR Fre" {} P0 | P1 ; Lock00: | Lock06: ; MOV EBX,$1 | MOV EBX,$1 ; XCHG [L_y],EBX | XCHG [L_x],EBX ; CMP EBX,$0 | CMP EBX,$0 ; JE Lock02 | JE Lock08 ; Lock01: | Lock07: ; MOV EBX,[L_y] | MOV EBX,[L_x] ; CMP EBX,$0 | CMP EBX,$0 ; JE Lock00 | JE Lock06 ; JMP Lock01 | JMP Lock07 ; Lock02: | Lock08: ; MOV [y],$1 | MOV [x],$1 ; MOV [L_y],$0 | MOV [L_x],$0 ; Lock03: | Lock09: ; MOV EBX,$1 | MOV EBX,$1 ; XCHG [L_x],EBX | XCHG [L_y],EBX ; CMP EBX,$0 | CMP EBX,$0 ; JE Lock05 | JE Lock11 ; Lock04: | Lock10: ; MOV EBX,[L_x] | MOV EBX,[L_y] ; CMP EBX,$0 | CMP EBX,$0 ; JE Lock03 | JE Lock09 ; JMP Lock04 | JMP Lock10 ; Lock05: | Lock11: ; MOV EAX,[x] | MOV EAX,[y] ; MOV [L_x],$0 | MOV [L_y],$0 ; exists (0:EAX=0 /\ 1:EAX=0) Generated assembler _litmus_P1_0_: cmpl $0,%edx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: LitLock06: _litmus_P1_4_: movl $1,%r12d _litmus_P1_5_: xchgl %r12d,(%r9) _litmus_P1_6_: cmpl $0,%r12d _litmus_P1_7_: je LitLock08 _litmus_P1_8_: LitLock07: _litmus_P1_9_: movl (%r9),%r12d _litmus_P1_10_: cmpl $0,%r12d _litmus_P1_11_: je LitLock06 _litmus_P1_12_: jmp LitLock07 _litmus_P1_13_: LitLock08: _litmus_P1_14_: movl $1,(%rbp) _litmus_P1_15_: movl $0,(%r9) _litmus_P1_16_: LitLock09: _litmus_P1_17_: movl $1,%r12d _litmus_P1_18_: xchgl %r12d,(%r8) _litmus_P1_19_: cmpl $0,%r12d _litmus_P1_20_: je LitLock11 _litmus_P1_21_: LitLock10: _litmus_P1_22_: movl (%r8),%r12d _litmus_P1_23_: cmpl $0,%r12d _litmus_P1_24_: je LitLock09 _litmus_P1_25_: jmp LitLock10 _litmus_P1_26_: LitLock11: _litmus_P1_27_: movl (%rdi),%eax _litmus_P1_28_: movl $0,(%r8) _litmus_P1_29_: decl %edx _litmus_P1_30_: Lit__L3: _litmus_P1_31_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%edx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: LitLock00: _litmus_P0_4_: movl $1,%r12d _litmus_P0_5_: xchgl %r12d,(%r8) _litmus_P0_6_: cmpl $0,%r12d _litmus_P0_7_: je LitLock02 _litmus_P0_8_: LitLock01: _litmus_P0_9_: movl (%r8),%r12d _litmus_P0_10_: cmpl $0,%r12d _litmus_P0_11_: je LitLock00 _litmus_P0_12_: jmp LitLock01 _litmus_P0_13_: LitLock02: _litmus_P0_14_: movl $1,(%rdi) _litmus_P0_15_: movl $0,(%r8) _litmus_P0_16_: LitLock03: _litmus_P0_17_: movl $1,%r12d _litmus_P0_18_: xchgl %r12d,(%r9) _litmus_P0_19_: cmpl $0,%r12d _litmus_P0_20_: je LitLock05 _litmus_P0_21_: LitLock04: _litmus_P0_22_: movl (%r9),%r12d _litmus_P0_23_: cmpl $0,%r12d _litmus_P0_24_: je LitLock03 _litmus_P0_25_: jmp LitLock04 _litmus_P0_26_: LitLock05: _litmus_P0_27_: movl (%rbp),%eax _litmus_P0_28_: movl $0,(%r9) _litmus_P0_29_: decl %edx _litmus_P0_30_: Lit__L1: _litmus_P0_31_: jg Lit__L0 Test L02 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0) is NOT validated Hash=8496c37f99fa3ca2b56c4ea54c3369fb Observation L02 Never 0 1 Time L02 60.74 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/L03.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 L03 "PodWR Fre PodWR Fre PodWR Fre" {} P0 | P1 | P2 ; Lock00: | Lock06: | Lock12: ; MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 ; XCHG [L_z],EBX | XCHG [L_x],EBX | XCHG [L_y],EBX ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock02 | JE Lock08 | JE Lock14 ; Lock01: | Lock07: | Lock13: ; MOV EBX,[L_z] | MOV EBX,[L_x] | MOV EBX,[L_y] ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock00 | JE Lock06 | JE Lock12 ; JMP Lock01 | JMP Lock07 | JMP Lock13 ; Lock02: | Lock08: | Lock14: ; MOV [z],$1 | MOV [x],$1 | MOV [y],$1 ; MOV [L_z],$0 | MOV [L_x],$0 | MOV [L_y],$0 ; Lock03: | Lock09: | Lock15: ; MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 ; XCHG [L_x],EBX | XCHG [L_y],EBX | XCHG [L_z],EBX ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock05 | JE Lock11 | JE Lock17 ; Lock04: | Lock10: | Lock16: ; MOV EBX,[L_x] | MOV EBX,[L_y] | MOV EBX,[L_z] ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock03 | JE Lock09 | JE Lock15 ; JMP Lock04 | JMP Lock10 | JMP Lock16 ; Lock05: | Lock11: | Lock17: ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] ; MOV [L_x],$0 | MOV [L_y],$0 | MOV [L_z],$0 ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0) Generated assembler _litmus_P2_0_: cmpl $0,%edx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: LitLock12: _litmus_P2_4_: movl $1,%r13d _litmus_P2_5_: xchgl %r13d,(%r11) _litmus_P2_6_: cmpl $0,%r13d _litmus_P2_7_: je LitLock14 _litmus_P2_8_: LitLock13: _litmus_P2_9_: movl (%r11),%r13d _litmus_P2_10_: cmpl $0,%r13d _litmus_P2_11_: je LitLock12 _litmus_P2_12_: jmp LitLock13 _litmus_P2_13_: LitLock14: _litmus_P2_14_: movl $1,(%r9) _litmus_P2_15_: movl $0,(%r11) _litmus_P2_16_: LitLock15: _litmus_P2_17_: movl $1,%r13d _litmus_P2_18_: xchgl %r13d,(%r10) _litmus_P2_19_: cmpl $0,%r13d _litmus_P2_20_: je LitLock17 _litmus_P2_21_: LitLock16: _litmus_P2_22_: movl (%r10),%r13d _litmus_P2_23_: cmpl $0,%r13d _litmus_P2_24_: je LitLock15 _litmus_P2_25_: jmp LitLock16 _litmus_P2_26_: LitLock17: _litmus_P2_27_: movl (%r8),%eax _litmus_P2_28_: movl $0,(%r10) _litmus_P2_29_: decl %edx _litmus_P2_30_: Lit__L5: _litmus_P2_31_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%edx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: LitLock06: _litmus_P1_4_: movl $1,%r13d _litmus_P1_5_: xchgl %r13d,(%r11) _litmus_P1_6_: cmpl $0,%r13d _litmus_P1_7_: je LitLock08 _litmus_P1_8_: LitLock07: _litmus_P1_9_: movl (%r11),%r13d _litmus_P1_10_: cmpl $0,%r13d _litmus_P1_11_: je LitLock06 _litmus_P1_12_: jmp LitLock07 _litmus_P1_13_: LitLock08: _litmus_P1_14_: movl $1,(%r9) _litmus_P1_15_: movl $0,(%r11) _litmus_P1_16_: LitLock09: _litmus_P1_17_: movl $1,%r13d _litmus_P1_18_: xchgl %r13d,(%r10) _litmus_P1_19_: cmpl $0,%r13d _litmus_P1_20_: je LitLock11 _litmus_P1_21_: LitLock10: _litmus_P1_22_: movl (%r10),%r13d _litmus_P1_23_: cmpl $0,%r13d _litmus_P1_24_: je LitLock09 _litmus_P1_25_: jmp LitLock10 _litmus_P1_26_: LitLock11: _litmus_P1_27_: movl (%r8),%eax _litmus_P1_28_: movl $0,(%r10) _litmus_P1_29_: decl %edx _litmus_P1_30_: Lit__L3: _litmus_P1_31_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%edx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: LitLock00: _litmus_P0_4_: movl $1,%r13d _litmus_P0_5_: xchgl %r13d,(%r10) _litmus_P0_6_: cmpl $0,%r13d _litmus_P0_7_: je LitLock02 _litmus_P0_8_: LitLock01: _litmus_P0_9_: movl (%r10),%r13d _litmus_P0_10_: cmpl $0,%r13d _litmus_P0_11_: je LitLock00 _litmus_P0_12_: jmp LitLock01 _litmus_P0_13_: LitLock02: _litmus_P0_14_: movl $1,(%r8) _litmus_P0_15_: movl $0,(%r10) _litmus_P0_16_: LitLock03: _litmus_P0_17_: movl $1,%r13d _litmus_P0_18_: xchgl %r13d,(%r11) _litmus_P0_19_: cmpl $0,%r13d _litmus_P0_20_: je LitLock05 _litmus_P0_21_: LitLock04: _litmus_P0_22_: movl (%r11),%r13d _litmus_P0_23_: cmpl $0,%r13d _litmus_P0_24_: je LitLock03 _litmus_P0_25_: jmp LitLock04 _litmus_P0_26_: LitLock05: _litmus_P0_27_: movl (%r9),%eax _litmus_P0_28_: movl $0,(%r11) _litmus_P0_29_: decl %edx _litmus_P0_30_: Lit__L1: _litmus_P0_31_: jg Lit__L0 Test L03 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0) is NOT validated Hash=f6bd7872ec42b5555a4a656473af2bb3 Observation L03 Never 0 1 Time L03 67.88 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/L04.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 L04 "PodWR Fre PodWR Fre PodWR Fre PodWR Fre" {} P0 | P1 | P2 | P3 ; Lock00: | Lock06: | Lock12: | Lock18: ; MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 ; XCHG [L_a],EBX | XCHG [L_x],EBX | XCHG [L_y],EBX | XCHG [L_z],EBX ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock02 | JE Lock08 | JE Lock14 | JE Lock20 ; Lock01: | Lock07: | Lock13: | Lock19: ; MOV EBX,[L_a] | MOV EBX,[L_x] | MOV EBX,[L_y] | MOV EBX,[L_z] ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock00 | JE Lock06 | JE Lock12 | JE Lock18 ; JMP Lock01 | JMP Lock07 | JMP Lock13 | JMP Lock19 ; Lock02: | Lock08: | Lock14: | Lock20: ; MOV [a],$1 | MOV [x],$1 | MOV [y],$1 | MOV [z],$1 ; MOV [L_a],$0 | MOV [L_x],$0 | MOV [L_y],$0 | MOV [L_z],$0 ; Lock03: | Lock09: | Lock15: | Lock21: ; MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 ; XCHG [L_x],EBX | XCHG [L_y],EBX | XCHG [L_z],EBX | XCHG [L_a],EBX ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock05 | JE Lock11 | JE Lock17 | JE Lock23 ; Lock04: | Lock10: | Lock16: | Lock22: ; MOV EBX,[L_x] | MOV EBX,[L_y] | MOV EBX,[L_z] | MOV EBX,[L_a] ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock03 | JE Lock09 | JE Lock15 | JE Lock21 ; JMP Lock04 | JMP Lock10 | JMP Lock16 | JMP Lock22 ; Lock05: | Lock11: | Lock17: | Lock23: ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] | MOV EAX,[a] ; MOV [L_x],$0 | MOV [L_y],$0 | MOV [L_z],$0 | MOV [L_a],$0 ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0) Generated assembler _litmus_P3_0_: cmpl $0,%edx _litmus_P3_1_: jmp Lit__L7 _litmus_P3_2_: Lit__L6: _litmus_P3_3_: LitLock18: _litmus_P3_4_: movl $1,%r12d _litmus_P3_5_: xchgl %r12d,(%r8) _litmus_P3_6_: cmpl $0,%r12d _litmus_P3_7_: je LitLock20 _litmus_P3_8_: LitLock19: _litmus_P3_9_: movl (%r8),%r12d _litmus_P3_10_: cmpl $0,%r12d _litmus_P3_11_: je LitLock18 _litmus_P3_12_: jmp LitLock19 _litmus_P3_13_: LitLock20: _litmus_P3_14_: movl $1,(%rdi) _litmus_P3_15_: movl $0,(%r8) _litmus_P3_16_: LitLock21: _litmus_P3_17_: movl $1,%r12d _litmus_P3_18_: xchgl %r12d,(%r9) _litmus_P3_19_: cmpl $0,%r12d _litmus_P3_20_: je LitLock23 _litmus_P3_21_: LitLock22: _litmus_P3_22_: movl (%r9),%r12d _litmus_P3_23_: cmpl $0,%r12d _litmus_P3_24_: je LitLock21 _litmus_P3_25_: jmp LitLock22 _litmus_P3_26_: LitLock23: _litmus_P3_27_: movl (%rbp),%eax _litmus_P3_28_: movl $0,(%r9) _litmus_P3_29_: decl %edx _litmus_P3_30_: Lit__L7: _litmus_P3_31_: jg Lit__L6 _litmus_P2_0_: cmpl $0,%edx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: LitLock12: _litmus_P2_4_: movl $1,%r12d _litmus_P2_5_: xchgl %r12d,(%r9) _litmus_P2_6_: cmpl $0,%r12d _litmus_P2_7_: je LitLock14 _litmus_P2_8_: LitLock13: _litmus_P2_9_: movl (%r9),%r12d _litmus_P2_10_: cmpl $0,%r12d _litmus_P2_11_: je LitLock12 _litmus_P2_12_: jmp LitLock13 _litmus_P2_13_: LitLock14: _litmus_P2_14_: movl $1,(%rbp) _litmus_P2_15_: movl $0,(%r9) _litmus_P2_16_: LitLock15: _litmus_P2_17_: movl $1,%r12d _litmus_P2_18_: xchgl %r12d,(%r8) _litmus_P2_19_: cmpl $0,%r12d _litmus_P2_20_: je LitLock17 _litmus_P2_21_: LitLock16: _litmus_P2_22_: movl (%r8),%r12d _litmus_P2_23_: cmpl $0,%r12d _litmus_P2_24_: je LitLock15 _litmus_P2_25_: jmp LitLock16 _litmus_P2_26_: LitLock17: _litmus_P2_27_: movl (%rdi),%eax _litmus_P2_28_: movl $0,(%r8) _litmus_P2_29_: decl %edx _litmus_P2_30_: Lit__L5: _litmus_P2_31_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%edx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: LitLock06: _litmus_P1_4_: movl $1,%r12d _litmus_P1_5_: xchgl %r12d,(%r9) _litmus_P1_6_: cmpl $0,%r12d _litmus_P1_7_: je LitLock08 _litmus_P1_8_: LitLock07: _litmus_P1_9_: movl (%r9),%r12d _litmus_P1_10_: cmpl $0,%r12d _litmus_P1_11_: je LitLock06 _litmus_P1_12_: jmp LitLock07 _litmus_P1_13_: LitLock08: _litmus_P1_14_: movl $1,(%rbp) _litmus_P1_15_: movl $0,(%r9) _litmus_P1_16_: LitLock09: _litmus_P1_17_: movl $1,%r12d _litmus_P1_18_: xchgl %r12d,(%r8) _litmus_P1_19_: cmpl $0,%r12d _litmus_P1_20_: je LitLock11 _litmus_P1_21_: LitLock10: _litmus_P1_22_: movl (%r8),%r12d _litmus_P1_23_: cmpl $0,%r12d _litmus_P1_24_: je LitLock09 _litmus_P1_25_: jmp LitLock10 _litmus_P1_26_: LitLock11: _litmus_P1_27_: movl (%rdi),%eax _litmus_P1_28_: movl $0,(%r8) _litmus_P1_29_: decl %edx _litmus_P1_30_: Lit__L3: _litmus_P1_31_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%edx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: LitLock00: _litmus_P0_4_: movl $1,%r12d _litmus_P0_5_: xchgl %r12d,(%r9) _litmus_P0_6_: cmpl $0,%r12d _litmus_P0_7_: je LitLock02 _litmus_P0_8_: LitLock01: _litmus_P0_9_: movl (%r9),%r12d _litmus_P0_10_: cmpl $0,%r12d _litmus_P0_11_: je LitLock00 _litmus_P0_12_: jmp LitLock01 _litmus_P0_13_: LitLock02: _litmus_P0_14_: movl $1,(%rbp) _litmus_P0_15_: movl $0,(%r9) _litmus_P0_16_: LitLock03: _litmus_P0_17_: movl $1,%r12d _litmus_P0_18_: xchgl %r12d,(%r8) _litmus_P0_19_: cmpl $0,%r12d _litmus_P0_20_: je LitLock05 _litmus_P0_21_: LitLock04: _litmus_P0_22_: movl (%r8),%r12d _litmus_P0_23_: cmpl $0,%r12d _litmus_P0_24_: je LitLock03 _litmus_P0_25_: jmp LitLock04 _litmus_P0_26_: LitLock05: _litmus_P0_27_: movl (%rdi),%eax _litmus_P0_28_: movl $0,(%r8) _litmus_P0_29_: decl %edx _litmus_P0_30_: Lit__L1: _litmus_P0_31_: jg Lit__L0 Test L04 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; 3:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0) is NOT validated Hash=b1210f205cc76920bb5b061f145f7cd6 Observation L04 Never 0 1 Time L04 80.58 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/L05.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 L05 "PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre" {} P0 | P1 | P2 | P3 | P4 ; Lock00: | Lock06: | Lock12: | Lock18: | Lock24: ; MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 ; XCHG [L_b],EBX | XCHG [L_x],EBX | XCHG [L_y],EBX | XCHG [L_z],EBX | XCHG [L_a],EBX ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock02 | JE Lock08 | JE Lock14 | JE Lock20 | JE Lock26 ; Lock01: | Lock07: | Lock13: | Lock19: | Lock25: ; MOV EBX,[L_b] | MOV EBX,[L_x] | MOV EBX,[L_y] | MOV EBX,[L_z] | MOV EBX,[L_a] ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock00 | JE Lock06 | JE Lock12 | JE Lock18 | JE Lock24 ; JMP Lock01 | JMP Lock07 | JMP Lock13 | JMP Lock19 | JMP Lock25 ; Lock02: | Lock08: | Lock14: | Lock20: | Lock26: ; MOV [b],$1 | MOV [x],$1 | MOV [y],$1 | MOV [z],$1 | MOV [a],$1 ; MOV [L_b],$0 | MOV [L_x],$0 | MOV [L_y],$0 | MOV [L_z],$0 | MOV [L_a],$0 ; Lock03: | Lock09: | Lock15: | Lock21: | Lock27: ; MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 ; XCHG [L_x],EBX | XCHG [L_y],EBX | XCHG [L_z],EBX | XCHG [L_a],EBX | XCHG [L_b],EBX ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock05 | JE Lock11 | JE Lock17 | JE Lock23 | JE Lock29 ; Lock04: | Lock10: | Lock16: | Lock22: | Lock28: ; MOV EBX,[L_x] | MOV EBX,[L_y] | MOV EBX,[L_z] | MOV EBX,[L_a] | MOV EBX,[L_b] ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock03 | JE Lock09 | JE Lock15 | JE Lock21 | JE Lock27 ; JMP Lock04 | JMP Lock10 | JMP Lock16 | JMP Lock22 | JMP Lock28 ; Lock05: | Lock11: | Lock17: | Lock23: | Lock29: ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] | MOV EAX,[a] | MOV EAX,[b] ; MOV [L_x],$0 | MOV [L_y],$0 | MOV [L_z],$0 | MOV [L_a],$0 | MOV [L_b],$0 ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0) Generated assembler _litmus_P4_0_: cmpl $0,%edx _litmus_P4_1_: jmp Lit__L9 _litmus_P4_2_: Lit__L8: _litmus_P4_3_: LitLock24: _litmus_P4_4_: movl $1,%r13d _litmus_P4_5_: xchgl %r13d,(%r11) _litmus_P4_6_: cmpl $0,%r13d _litmus_P4_7_: je LitLock26 _litmus_P4_8_: LitLock25: _litmus_P4_9_: movl (%r11),%r13d _litmus_P4_10_: cmpl $0,%r13d _litmus_P4_11_: je LitLock24 _litmus_P4_12_: jmp LitLock25 _litmus_P4_13_: LitLock26: _litmus_P4_14_: movl $1,(%r9) _litmus_P4_15_: movl $0,(%r11) _litmus_P4_16_: LitLock27: _litmus_P4_17_: movl $1,%r13d _litmus_P4_18_: xchgl %r13d,(%r10) _litmus_P4_19_: cmpl $0,%r13d _litmus_P4_20_: je LitLock29 _litmus_P4_21_: LitLock28: _litmus_P4_22_: movl (%r10),%r13d _litmus_P4_23_: cmpl $0,%r13d _litmus_P4_24_: je LitLock27 _litmus_P4_25_: jmp LitLock28 _litmus_P4_26_: LitLock29: _litmus_P4_27_: movl (%r8),%eax _litmus_P4_28_: movl $0,(%r10) _litmus_P4_29_: decl %edx _litmus_P4_30_: Lit__L9: _litmus_P4_31_: jg Lit__L8 _litmus_P3_0_: cmpl $0,%edx _litmus_P3_1_: jmp Lit__L7 _litmus_P3_2_: Lit__L6: _litmus_P3_3_: LitLock18: _litmus_P3_4_: movl $1,%r13d _litmus_P3_5_: xchgl %r13d,(%r10) _litmus_P3_6_: cmpl $0,%r13d _litmus_P3_7_: je LitLock20 _litmus_P3_8_: LitLock19: _litmus_P3_9_: movl (%r10),%r13d _litmus_P3_10_: cmpl $0,%r13d _litmus_P3_11_: je LitLock18 _litmus_P3_12_: jmp LitLock19 _litmus_P3_13_: LitLock20: _litmus_P3_14_: movl $1,(%r8) _litmus_P3_15_: movl $0,(%r10) _litmus_P3_16_: LitLock21: _litmus_P3_17_: movl $1,%r13d _litmus_P3_18_: xchgl %r13d,(%r11) _litmus_P3_19_: cmpl $0,%r13d _litmus_P3_20_: je LitLock23 _litmus_P3_21_: LitLock22: _litmus_P3_22_: movl (%r11),%r13d _litmus_P3_23_: cmpl $0,%r13d _litmus_P3_24_: je LitLock21 _litmus_P3_25_: jmp LitLock22 _litmus_P3_26_: LitLock23: _litmus_P3_27_: movl (%r9),%eax _litmus_P3_28_: movl $0,(%r11) _litmus_P3_29_: decl %edx _litmus_P3_30_: Lit__L7: _litmus_P3_31_: jg Lit__L6 _litmus_P2_0_: cmpl $0,%edx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: LitLock12: _litmus_P2_4_: movl $1,%r13d _litmus_P2_5_: xchgl %r13d,(%r11) _litmus_P2_6_: cmpl $0,%r13d _litmus_P2_7_: je LitLock14 _litmus_P2_8_: LitLock13: _litmus_P2_9_: movl (%r11),%r13d _litmus_P2_10_: cmpl $0,%r13d _litmus_P2_11_: je LitLock12 _litmus_P2_12_: jmp LitLock13 _litmus_P2_13_: LitLock14: _litmus_P2_14_: movl $1,(%r9) _litmus_P2_15_: movl $0,(%r11) _litmus_P2_16_: LitLock15: _litmus_P2_17_: movl $1,%r13d _litmus_P2_18_: xchgl %r13d,(%r10) _litmus_P2_19_: cmpl $0,%r13d _litmus_P2_20_: je LitLock17 _litmus_P2_21_: LitLock16: _litmus_P2_22_: movl (%r10),%r13d _litmus_P2_23_: cmpl $0,%r13d _litmus_P2_24_: je LitLock15 _litmus_P2_25_: jmp LitLock16 _litmus_P2_26_: LitLock17: _litmus_P2_27_: movl (%r8),%eax _litmus_P2_28_: movl $0,(%r10) _litmus_P2_29_: decl %edx _litmus_P2_30_: Lit__L5: _litmus_P2_31_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%edx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: LitLock06: _litmus_P1_4_: movl $1,%r13d _litmus_P1_5_: xchgl %r13d,(%r11) _litmus_P1_6_: cmpl $0,%r13d _litmus_P1_7_: je LitLock08 _litmus_P1_8_: LitLock07: _litmus_P1_9_: movl (%r11),%r13d _litmus_P1_10_: cmpl $0,%r13d _litmus_P1_11_: je LitLock06 _litmus_P1_12_: jmp LitLock07 _litmus_P1_13_: LitLock08: _litmus_P1_14_: movl $1,(%r9) _litmus_P1_15_: movl $0,(%r11) _litmus_P1_16_: LitLock09: _litmus_P1_17_: movl $1,%r13d _litmus_P1_18_: xchgl %r13d,(%r10) _litmus_P1_19_: cmpl $0,%r13d _litmus_P1_20_: je LitLock11 _litmus_P1_21_: LitLock10: _litmus_P1_22_: movl (%r10),%r13d _litmus_P1_23_: cmpl $0,%r13d _litmus_P1_24_: je LitLock09 _litmus_P1_25_: jmp LitLock10 _litmus_P1_26_: LitLock11: _litmus_P1_27_: movl (%r8),%eax _litmus_P1_28_: movl $0,(%r10) _litmus_P1_29_: decl %edx _litmus_P1_30_: Lit__L3: _litmus_P1_31_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%edx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: LitLock00: _litmus_P0_4_: movl $1,%r13d _litmus_P0_5_: xchgl %r13d,(%r11) _litmus_P0_6_: cmpl $0,%r13d _litmus_P0_7_: je LitLock02 _litmus_P0_8_: LitLock01: _litmus_P0_9_: movl (%r11),%r13d _litmus_P0_10_: cmpl $0,%r13d _litmus_P0_11_: je LitLock00 _litmus_P0_12_: jmp LitLock01 _litmus_P0_13_: LitLock02: _litmus_P0_14_: movl $1,(%r9) _litmus_P0_15_: movl $0,(%r11) _litmus_P0_16_: LitLock03: _litmus_P0_17_: movl $1,%r13d _litmus_P0_18_: xchgl %r13d,(%r10) _litmus_P0_19_: cmpl $0,%r13d _litmus_P0_20_: je LitLock05 _litmus_P0_21_: LitLock04: _litmus_P0_22_: movl (%r10),%r13d _litmus_P0_23_: cmpl $0,%r13d _litmus_P0_24_: je LitLock03 _litmus_P0_25_: jmp LitLock04 _litmus_P0_26_: LitLock05: _litmus_P0_27_: movl (%r8),%eax _litmus_P0_28_: movl $0,(%r10) _litmus_P0_29_: decl %edx _litmus_P0_30_: Lit__L1: _litmus_P0_31_: jg Lit__L0 Test L05 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; 3:EAX=1; 4:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0) is NOT validated Hash=facb9dfea9e21810fbfa1bf6e4e44ecf Observation L05 Never 0 1 Time L05 86.55 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/L06.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 L06 "PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre" {} P0 | P1 | P2 | P3 | P4 | P5 ; Lock00: | Lock06: | Lock12: | Lock18: | Lock24: | Lock30: ; MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 ; XCHG [L_c],EBX | XCHG [L_x],EBX | XCHG [L_y],EBX | XCHG [L_z],EBX | XCHG [L_a],EBX | XCHG [L_b],EBX ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock02 | JE Lock08 | JE Lock14 | JE Lock20 | JE Lock26 | JE Lock32 ; Lock01: | Lock07: | Lock13: | Lock19: | Lock25: | Lock31: ; MOV EBX,[L_c] | MOV EBX,[L_x] | MOV EBX,[L_y] | MOV EBX,[L_z] | MOV EBX,[L_a] | MOV EBX,[L_b] ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock00 | JE Lock06 | JE Lock12 | JE Lock18 | JE Lock24 | JE Lock30 ; JMP Lock01 | JMP Lock07 | JMP Lock13 | JMP Lock19 | JMP Lock25 | JMP Lock31 ; Lock02: | Lock08: | Lock14: | Lock20: | Lock26: | Lock32: ; MOV [c],$1 | MOV [x],$1 | MOV [y],$1 | MOV [z],$1 | MOV [a],$1 | MOV [b],$1 ; MOV [L_c],$0 | MOV [L_x],$0 | MOV [L_y],$0 | MOV [L_z],$0 | MOV [L_a],$0 | MOV [L_b],$0 ; Lock03: | Lock09: | Lock15: | Lock21: | Lock27: | Lock33: ; MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 ; XCHG [L_x],EBX | XCHG [L_y],EBX | XCHG [L_z],EBX | XCHG [L_a],EBX | XCHG [L_b],EBX | XCHG [L_c],EBX ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock05 | JE Lock11 | JE Lock17 | JE Lock23 | JE Lock29 | JE Lock35 ; Lock04: | Lock10: | Lock16: | Lock22: | Lock28: | Lock34: ; MOV EBX,[L_x] | MOV EBX,[L_y] | MOV EBX,[L_z] | MOV EBX,[L_a] | MOV EBX,[L_b] | MOV EBX,[L_c] ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock03 | JE Lock09 | JE Lock15 | JE Lock21 | JE Lock27 | JE Lock33 ; JMP Lock04 | JMP Lock10 | JMP Lock16 | JMP Lock22 | JMP Lock28 | JMP Lock34 ; Lock05: | Lock11: | Lock17: | Lock23: | Lock29: | Lock35: ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] | MOV EAX,[a] | MOV EAX,[b] | MOV EAX,[c] ; MOV [L_x],$0 | MOV [L_y],$0 | MOV [L_z],$0 | MOV [L_a],$0 | MOV [L_b],$0 | MOV [L_c],$0 ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0) Generated assembler _litmus_P5_0_: cmpl $0,%edx _litmus_P5_1_: jmp Lit__L11 _litmus_P5_2_: Lit__L10: _litmus_P5_3_: LitLock30: _litmus_P5_4_: movl $1,%r13d _litmus_P5_5_: xchgl %r13d,(%r11) _litmus_P5_6_: cmpl $0,%r13d _litmus_P5_7_: je LitLock32 _litmus_P5_8_: LitLock31: _litmus_P5_9_: movl (%r11),%r13d _litmus_P5_10_: cmpl $0,%r13d _litmus_P5_11_: je LitLock30 _litmus_P5_12_: jmp LitLock31 _litmus_P5_13_: LitLock32: _litmus_P5_14_: movl $1,(%r9) _litmus_P5_15_: movl $0,(%r11) _litmus_P5_16_: LitLock33: _litmus_P5_17_: movl $1,%r13d _litmus_P5_18_: xchgl %r13d,(%r10) _litmus_P5_19_: cmpl $0,%r13d _litmus_P5_20_: je LitLock35 _litmus_P5_21_: LitLock34: _litmus_P5_22_: movl (%r10),%r13d _litmus_P5_23_: cmpl $0,%r13d _litmus_P5_24_: je LitLock33 _litmus_P5_25_: jmp LitLock34 _litmus_P5_26_: LitLock35: _litmus_P5_27_: movl (%r8),%eax _litmus_P5_28_: movl $0,(%r10) _litmus_P5_29_: decl %edx _litmus_P5_30_: Lit__L11: _litmus_P5_31_: jg Lit__L10 _litmus_P4_0_: cmpl $0,%edx _litmus_P4_1_: jmp Lit__L9 _litmus_P4_2_: Lit__L8: _litmus_P4_3_: LitLock24: _litmus_P4_4_: movl $1,%r13d _litmus_P4_5_: xchgl %r13d,(%r11) _litmus_P4_6_: cmpl $0,%r13d _litmus_P4_7_: je LitLock26 _litmus_P4_8_: LitLock25: _litmus_P4_9_: movl (%r11),%r13d _litmus_P4_10_: cmpl $0,%r13d _litmus_P4_11_: je LitLock24 _litmus_P4_12_: jmp LitLock25 _litmus_P4_13_: LitLock26: _litmus_P4_14_: movl $1,(%r9) _litmus_P4_15_: movl $0,(%r11) _litmus_P4_16_: LitLock27: _litmus_P4_17_: movl $1,%r13d _litmus_P4_18_: xchgl %r13d,(%r10) _litmus_P4_19_: cmpl $0,%r13d _litmus_P4_20_: je LitLock29 _litmus_P4_21_: LitLock28: _litmus_P4_22_: movl (%r10),%r13d _litmus_P4_23_: cmpl $0,%r13d _litmus_P4_24_: je LitLock27 _litmus_P4_25_: jmp LitLock28 _litmus_P4_26_: LitLock29: _litmus_P4_27_: movl (%r8),%eax _litmus_P4_28_: movl $0,(%r10) _litmus_P4_29_: decl %edx _litmus_P4_30_: Lit__L9: _litmus_P4_31_: jg Lit__L8 _litmus_P3_0_: cmpl $0,%edx _litmus_P3_1_: jmp Lit__L7 _litmus_P3_2_: Lit__L6: _litmus_P3_3_: LitLock18: _litmus_P3_4_: movl $1,%r13d _litmus_P3_5_: xchgl %r13d,(%r10) _litmus_P3_6_: cmpl $0,%r13d _litmus_P3_7_: je LitLock20 _litmus_P3_8_: LitLock19: _litmus_P3_9_: movl (%r10),%r13d _litmus_P3_10_: cmpl $0,%r13d _litmus_P3_11_: je LitLock18 _litmus_P3_12_: jmp LitLock19 _litmus_P3_13_: LitLock20: _litmus_P3_14_: movl $1,(%r8) _litmus_P3_15_: movl $0,(%r10) _litmus_P3_16_: LitLock21: _litmus_P3_17_: movl $1,%r13d _litmus_P3_18_: xchgl %r13d,(%r11) _litmus_P3_19_: cmpl $0,%r13d _litmus_P3_20_: je LitLock23 _litmus_P3_21_: LitLock22: _litmus_P3_22_: movl (%r11),%r13d _litmus_P3_23_: cmpl $0,%r13d _litmus_P3_24_: je LitLock21 _litmus_P3_25_: jmp LitLock22 _litmus_P3_26_: LitLock23: _litmus_P3_27_: movl (%r9),%eax _litmus_P3_28_: movl $0,(%r11) _litmus_P3_29_: decl %edx _litmus_P3_30_: Lit__L7: _litmus_P3_31_: jg Lit__L6 _litmus_P2_0_: cmpl $0,%edx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: LitLock12: _litmus_P2_4_: movl $1,%r13d _litmus_P2_5_: xchgl %r13d,(%r11) _litmus_P2_6_: cmpl $0,%r13d _litmus_P2_7_: je LitLock14 _litmus_P2_8_: LitLock13: _litmus_P2_9_: movl (%r11),%r13d _litmus_P2_10_: cmpl $0,%r13d _litmus_P2_11_: je LitLock12 _litmus_P2_12_: jmp LitLock13 _litmus_P2_13_: LitLock14: _litmus_P2_14_: movl $1,(%r9) _litmus_P2_15_: movl $0,(%r11) _litmus_P2_16_: LitLock15: _litmus_P2_17_: movl $1,%r13d _litmus_P2_18_: xchgl %r13d,(%r10) _litmus_P2_19_: cmpl $0,%r13d _litmus_P2_20_: je LitLock17 _litmus_P2_21_: LitLock16: _litmus_P2_22_: movl (%r10),%r13d _litmus_P2_23_: cmpl $0,%r13d _litmus_P2_24_: je LitLock15 _litmus_P2_25_: jmp LitLock16 _litmus_P2_26_: LitLock17: _litmus_P2_27_: movl (%r8),%eax _litmus_P2_28_: movl $0,(%r10) _litmus_P2_29_: decl %edx _litmus_P2_30_: Lit__L5: _litmus_P2_31_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%edx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: LitLock06: _litmus_P1_4_: movl $1,%r13d _litmus_P1_5_: xchgl %r13d,(%r11) _litmus_P1_6_: cmpl $0,%r13d _litmus_P1_7_: je LitLock08 _litmus_P1_8_: LitLock07: _litmus_P1_9_: movl (%r11),%r13d _litmus_P1_10_: cmpl $0,%r13d _litmus_P1_11_: je LitLock06 _litmus_P1_12_: jmp LitLock07 _litmus_P1_13_: LitLock08: _litmus_P1_14_: movl $1,(%r9) _litmus_P1_15_: movl $0,(%r11) _litmus_P1_16_: LitLock09: _litmus_P1_17_: movl $1,%r13d _litmus_P1_18_: xchgl %r13d,(%r10) _litmus_P1_19_: cmpl $0,%r13d _litmus_P1_20_: je LitLock11 _litmus_P1_21_: LitLock10: _litmus_P1_22_: movl (%r10),%r13d _litmus_P1_23_: cmpl $0,%r13d _litmus_P1_24_: je LitLock09 _litmus_P1_25_: jmp LitLock10 _litmus_P1_26_: LitLock11: _litmus_P1_27_: movl (%r8),%eax _litmus_P1_28_: movl $0,(%r10) _litmus_P1_29_: decl %edx _litmus_P1_30_: Lit__L3: _litmus_P1_31_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%edx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: LitLock00: _litmus_P0_4_: movl $1,%r13d _litmus_P0_5_: xchgl %r13d,(%r11) _litmus_P0_6_: cmpl $0,%r13d _litmus_P0_7_: je LitLock02 _litmus_P0_8_: LitLock01: _litmus_P0_9_: movl (%r11),%r13d _litmus_P0_10_: cmpl $0,%r13d _litmus_P0_11_: je LitLock00 _litmus_P0_12_: jmp LitLock01 _litmus_P0_13_: LitLock02: _litmus_P0_14_: movl $1,(%r9) _litmus_P0_15_: movl $0,(%r11) _litmus_P0_16_: LitLock03: _litmus_P0_17_: movl $1,%r13d _litmus_P0_18_: xchgl %r13d,(%r10) _litmus_P0_19_: cmpl $0,%r13d _litmus_P0_20_: je LitLock05 _litmus_P0_21_: LitLock04: _litmus_P0_22_: movl (%r10),%r13d _litmus_P0_23_: cmpl $0,%r13d _litmus_P0_24_: je LitLock03 _litmus_P0_25_: jmp LitLock04 _litmus_P0_26_: LitLock05: _litmus_P0_27_: movl (%r8),%eax _litmus_P0_28_: movl $0,(%r10) _litmus_P0_29_: decl %edx _litmus_P0_30_: Lit__L1: _litmus_P0_31_: jg Lit__L0 Test L06 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; 3:EAX=1; 4:EAX=1; 5:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0) is NOT validated Hash=7c229b6e2119742b24a44736c832de0e Observation L06 Never 0 1 Time L06 94.78 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/L07.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 L07 "PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre" {} P0 | P1 | P2 | P3 | P4 | P5 | P6 ; Lock00: | Lock06: | Lock12: | Lock18: | Lock24: | Lock30: | Lock36: ; MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 ; XCHG [L_d],EBX | XCHG [L_x],EBX | XCHG [L_y],EBX | XCHG [L_z],EBX | XCHG [L_a],EBX | XCHG [L_b],EBX | XCHG [L_c],EBX ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock02 | JE Lock08 | JE Lock14 | JE Lock20 | JE Lock26 | JE Lock32 | JE Lock38 ; Lock01: | Lock07: | Lock13: | Lock19: | Lock25: | Lock31: | Lock37: ; MOV EBX,[L_d] | MOV EBX,[L_x] | MOV EBX,[L_y] | MOV EBX,[L_z] | MOV EBX,[L_a] | MOV EBX,[L_b] | MOV EBX,[L_c] ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock00 | JE Lock06 | JE Lock12 | JE Lock18 | JE Lock24 | JE Lock30 | JE Lock36 ; JMP Lock01 | JMP Lock07 | JMP Lock13 | JMP Lock19 | JMP Lock25 | JMP Lock31 | JMP Lock37 ; Lock02: | Lock08: | Lock14: | Lock20: | Lock26: | Lock32: | Lock38: ; MOV [d],$1 | MOV [x],$1 | MOV [y],$1 | MOV [z],$1 | MOV [a],$1 | MOV [b],$1 | MOV [c],$1 ; MOV [L_d],$0 | MOV [L_x],$0 | MOV [L_y],$0 | MOV [L_z],$0 | MOV [L_a],$0 | MOV [L_b],$0 | MOV [L_c],$0 ; Lock03: | Lock09: | Lock15: | Lock21: | Lock27: | Lock33: | Lock39: ; MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 ; XCHG [L_x],EBX | XCHG [L_y],EBX | XCHG [L_z],EBX | XCHG [L_a],EBX | XCHG [L_b],EBX | XCHG [L_c],EBX | XCHG [L_d],EBX ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock05 | JE Lock11 | JE Lock17 | JE Lock23 | JE Lock29 | JE Lock35 | JE Lock41 ; Lock04: | Lock10: | Lock16: | Lock22: | Lock28: | Lock34: | Lock40: ; MOV EBX,[L_x] | MOV EBX,[L_y] | MOV EBX,[L_z] | MOV EBX,[L_a] | MOV EBX,[L_b] | MOV EBX,[L_c] | MOV EBX,[L_d] ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock03 | JE Lock09 | JE Lock15 | JE Lock21 | JE Lock27 | JE Lock33 | JE Lock39 ; JMP Lock04 | JMP Lock10 | JMP Lock16 | JMP Lock22 | JMP Lock28 | JMP Lock34 | JMP Lock40 ; Lock05: | Lock11: | Lock17: | Lock23: | Lock29: | Lock35: | Lock41: ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] | MOV EAX,[a] | MOV EAX,[b] | MOV EAX,[c] | MOV EAX,[d] ; MOV [L_x],$0 | MOV [L_y],$0 | MOV [L_z],$0 | MOV [L_a],$0 | MOV [L_b],$0 | MOV [L_c],$0 | MOV [L_d],$0 ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0 /\ 6:EAX=0) Generated assembler _litmus_P6_0_: cmpl $0,%edx _litmus_P6_1_: jmp Lit__L13 _litmus_P6_2_: Lit__L12: _litmus_P6_3_: LitLock36: _litmus_P6_4_: movl $1,%r13d _litmus_P6_5_: xchgl %r13d,(%r11) _litmus_P6_6_: cmpl $0,%r13d _litmus_P6_7_: je LitLock38 _litmus_P6_8_: LitLock37: _litmus_P6_9_: movl (%r11),%r13d _litmus_P6_10_: cmpl $0,%r13d _litmus_P6_11_: je LitLock36 _litmus_P6_12_: jmp LitLock37 _litmus_P6_13_: LitLock38: _litmus_P6_14_: movl $1,(%r9) _litmus_P6_15_: movl $0,(%r11) _litmus_P6_16_: LitLock39: _litmus_P6_17_: movl $1,%r13d _litmus_P6_18_: xchgl %r13d,(%r10) _litmus_P6_19_: cmpl $0,%r13d _litmus_P6_20_: je LitLock41 _litmus_P6_21_: LitLock40: _litmus_P6_22_: movl (%r10),%r13d _litmus_P6_23_: cmpl $0,%r13d _litmus_P6_24_: je LitLock39 _litmus_P6_25_: jmp LitLock40 _litmus_P6_26_: LitLock41: _litmus_P6_27_: movl (%r8),%eax _litmus_P6_28_: movl $0,(%r10) _litmus_P6_29_: decl %edx _litmus_P6_30_: Lit__L13: _litmus_P6_31_: jg Lit__L12 _litmus_P5_0_: cmpl $0,%edx _litmus_P5_1_: jmp Lit__L11 _litmus_P5_2_: Lit__L10: _litmus_P5_3_: LitLock30: _litmus_P5_4_: movl $1,%r13d _litmus_P5_5_: xchgl %r13d,(%r11) _litmus_P5_6_: cmpl $0,%r13d _litmus_P5_7_: je LitLock32 _litmus_P5_8_: LitLock31: _litmus_P5_9_: movl (%r11),%r13d _litmus_P5_10_: cmpl $0,%r13d _litmus_P5_11_: je LitLock30 _litmus_P5_12_: jmp LitLock31 _litmus_P5_13_: LitLock32: _litmus_P5_14_: movl $1,(%r9) _litmus_P5_15_: movl $0,(%r11) _litmus_P5_16_: LitLock33: _litmus_P5_17_: movl $1,%r13d _litmus_P5_18_: xchgl %r13d,(%r10) _litmus_P5_19_: cmpl $0,%r13d _litmus_P5_20_: je LitLock35 _litmus_P5_21_: LitLock34: _litmus_P5_22_: movl (%r10),%r13d _litmus_P5_23_: cmpl $0,%r13d _litmus_P5_24_: je LitLock33 _litmus_P5_25_: jmp LitLock34 _litmus_P5_26_: LitLock35: _litmus_P5_27_: movl (%r8),%eax _litmus_P5_28_: movl $0,(%r10) _litmus_P5_29_: decl %edx _litmus_P5_30_: Lit__L11: _litmus_P5_31_: jg Lit__L10 _litmus_P4_0_: cmpl $0,%edx _litmus_P4_1_: jmp Lit__L9 _litmus_P4_2_: Lit__L8: _litmus_P4_3_: LitLock24: _litmus_P4_4_: movl $1,%r13d _litmus_P4_5_: xchgl %r13d,(%r11) _litmus_P4_6_: cmpl $0,%r13d _litmus_P4_7_: je LitLock26 _litmus_P4_8_: LitLock25: _litmus_P4_9_: movl (%r11),%r13d _litmus_P4_10_: cmpl $0,%r13d _litmus_P4_11_: je LitLock24 _litmus_P4_12_: jmp LitLock25 _litmus_P4_13_: LitLock26: _litmus_P4_14_: movl $1,(%r9) _litmus_P4_15_: movl $0,(%r11) _litmus_P4_16_: LitLock27: _litmus_P4_17_: movl $1,%r13d _litmus_P4_18_: xchgl %r13d,(%r10) _litmus_P4_19_: cmpl $0,%r13d _litmus_P4_20_: je LitLock29 _litmus_P4_21_: LitLock28: _litmus_P4_22_: movl (%r10),%r13d _litmus_P4_23_: cmpl $0,%r13d _litmus_P4_24_: je LitLock27 _litmus_P4_25_: jmp LitLock28 _litmus_P4_26_: LitLock29: _litmus_P4_27_: movl (%r8),%eax _litmus_P4_28_: movl $0,(%r10) _litmus_P4_29_: decl %edx _litmus_P4_30_: Lit__L9: _litmus_P4_31_: jg Lit__L8 _litmus_P3_0_: cmpl $0,%edx _litmus_P3_1_: jmp Lit__L7 _litmus_P3_2_: Lit__L6: _litmus_P3_3_: LitLock18: _litmus_P3_4_: movl $1,%r13d _litmus_P3_5_: xchgl %r13d,(%r10) _litmus_P3_6_: cmpl $0,%r13d _litmus_P3_7_: je LitLock20 _litmus_P3_8_: LitLock19: _litmus_P3_9_: movl (%r10),%r13d _litmus_P3_10_: cmpl $0,%r13d _litmus_P3_11_: je LitLock18 _litmus_P3_12_: jmp LitLock19 _litmus_P3_13_: LitLock20: _litmus_P3_14_: movl $1,(%r8) _litmus_P3_15_: movl $0,(%r10) _litmus_P3_16_: LitLock21: _litmus_P3_17_: movl $1,%r13d _litmus_P3_18_: xchgl %r13d,(%r11) _litmus_P3_19_: cmpl $0,%r13d _litmus_P3_20_: je LitLock23 _litmus_P3_21_: LitLock22: _litmus_P3_22_: movl (%r11),%r13d _litmus_P3_23_: cmpl $0,%r13d _litmus_P3_24_: je LitLock21 _litmus_P3_25_: jmp LitLock22 _litmus_P3_26_: LitLock23: _litmus_P3_27_: movl (%r9),%eax _litmus_P3_28_: movl $0,(%r11) _litmus_P3_29_: decl %edx _litmus_P3_30_: Lit__L7: _litmus_P3_31_: jg Lit__L6 _litmus_P2_0_: cmpl $0,%edx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: LitLock12: _litmus_P2_4_: movl $1,%r13d _litmus_P2_5_: xchgl %r13d,(%r11) _litmus_P2_6_: cmpl $0,%r13d _litmus_P2_7_: je LitLock14 _litmus_P2_8_: LitLock13: _litmus_P2_9_: movl (%r11),%r13d _litmus_P2_10_: cmpl $0,%r13d _litmus_P2_11_: je LitLock12 _litmus_P2_12_: jmp LitLock13 _litmus_P2_13_: LitLock14: _litmus_P2_14_: movl $1,(%r9) _litmus_P2_15_: movl $0,(%r11) _litmus_P2_16_: LitLock15: _litmus_P2_17_: movl $1,%r13d _litmus_P2_18_: xchgl %r13d,(%r10) _litmus_P2_19_: cmpl $0,%r13d _litmus_P2_20_: je LitLock17 _litmus_P2_21_: LitLock16: _litmus_P2_22_: movl (%r10),%r13d _litmus_P2_23_: cmpl $0,%r13d _litmus_P2_24_: je LitLock15 _litmus_P2_25_: jmp LitLock16 _litmus_P2_26_: LitLock17: _litmus_P2_27_: movl (%r8),%eax _litmus_P2_28_: movl $0,(%r10) _litmus_P2_29_: decl %edx _litmus_P2_30_: Lit__L5: _litmus_P2_31_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%edx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: LitLock06: _litmus_P1_4_: movl $1,%r13d _litmus_P1_5_: xchgl %r13d,(%r11) _litmus_P1_6_: cmpl $0,%r13d _litmus_P1_7_: je LitLock08 _litmus_P1_8_: LitLock07: _litmus_P1_9_: movl (%r11),%r13d _litmus_P1_10_: cmpl $0,%r13d _litmus_P1_11_: je LitLock06 _litmus_P1_12_: jmp LitLock07 _litmus_P1_13_: LitLock08: _litmus_P1_14_: movl $1,(%r9) _litmus_P1_15_: movl $0,(%r11) _litmus_P1_16_: LitLock09: _litmus_P1_17_: movl $1,%r13d _litmus_P1_18_: xchgl %r13d,(%r10) _litmus_P1_19_: cmpl $0,%r13d _litmus_P1_20_: je LitLock11 _litmus_P1_21_: LitLock10: _litmus_P1_22_: movl (%r10),%r13d _litmus_P1_23_: cmpl $0,%r13d _litmus_P1_24_: je LitLock09 _litmus_P1_25_: jmp LitLock10 _litmus_P1_26_: LitLock11: _litmus_P1_27_: movl (%r8),%eax _litmus_P1_28_: movl $0,(%r10) _litmus_P1_29_: decl %edx _litmus_P1_30_: Lit__L3: _litmus_P1_31_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%edx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: LitLock00: _litmus_P0_4_: movl $1,%r13d _litmus_P0_5_: xchgl %r13d,(%r11) _litmus_P0_6_: cmpl $0,%r13d _litmus_P0_7_: je LitLock02 _litmus_P0_8_: LitLock01: _litmus_P0_9_: movl (%r11),%r13d _litmus_P0_10_: cmpl $0,%r13d _litmus_P0_11_: je LitLock00 _litmus_P0_12_: jmp LitLock01 _litmus_P0_13_: LitLock02: _litmus_P0_14_: movl $1,(%r9) _litmus_P0_15_: movl $0,(%r11) _litmus_P0_16_: LitLock03: _litmus_P0_17_: movl $1,%r13d _litmus_P0_18_: xchgl %r13d,(%r10) _litmus_P0_19_: cmpl $0,%r13d _litmus_P0_20_: je LitLock05 _litmus_P0_21_: LitLock04: _litmus_P0_22_: movl (%r10),%r13d _litmus_P0_23_: cmpl $0,%r13d _litmus_P0_24_: je LitLock03 _litmus_P0_25_: jmp LitLock04 _litmus_P0_26_: LitLock05: _litmus_P0_27_: movl (%r8),%eax _litmus_P0_28_: movl $0,(%r10) _litmus_P0_29_: decl %edx _litmus_P0_30_: Lit__L1: _litmus_P0_31_: jg Lit__L0 Test L07 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; 3:EAX=1; 4:EAX=1; 5:EAX=1; 6:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0 /\ 6:EAX=0) is NOT validated Hash=e0ad1cc1615528a57c39f1bb9b102756 Observation L07 Never 0 1 Time L07 99.07 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Results for PodWR/L08.litmus % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% X86 L08 "PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre PodWR Fre" {} P0 | P1 | P2 | P3 | P4 | P5 | P6 | P7 ; Lock00: | Lock06: | Lock12: | Lock18: | Lock24: | Lock30: | Lock36: | Lock42: ; MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 ; XCHG [L_e],EBX | XCHG [L_x],EBX | XCHG [L_y],EBX | XCHG [L_z],EBX | XCHG [L_a],EBX | XCHG [L_b],EBX | XCHG [L_c],EBX | XCHG [L_d],EBX ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock02 | JE Lock08 | JE Lock14 | JE Lock20 | JE Lock26 | JE Lock32 | JE Lock38 | JE Lock44 ; Lock01: | Lock07: | Lock13: | Lock19: | Lock25: | Lock31: | Lock37: | Lock43: ; MOV EBX,[L_e] | MOV EBX,[L_x] | MOV EBX,[L_y] | MOV EBX,[L_z] | MOV EBX,[L_a] | MOV EBX,[L_b] | MOV EBX,[L_c] | MOV EBX,[L_d] ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock00 | JE Lock06 | JE Lock12 | JE Lock18 | JE Lock24 | JE Lock30 | JE Lock36 | JE Lock42 ; JMP Lock01 | JMP Lock07 | JMP Lock13 | JMP Lock19 | JMP Lock25 | JMP Lock31 | JMP Lock37 | JMP Lock43 ; Lock02: | Lock08: | Lock14: | Lock20: | Lock26: | Lock32: | Lock38: | Lock44: ; MOV [e],$1 | MOV [x],$1 | MOV [y],$1 | MOV [z],$1 | MOV [a],$1 | MOV [b],$1 | MOV [c],$1 | MOV [d],$1 ; MOV [L_e],$0 | MOV [L_x],$0 | MOV [L_y],$0 | MOV [L_z],$0 | MOV [L_a],$0 | MOV [L_b],$0 | MOV [L_c],$0 | MOV [L_d],$0 ; Lock03: | Lock09: | Lock15: | Lock21: | Lock27: | Lock33: | Lock39: | Lock45: ; MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 | MOV EBX,$1 ; XCHG [L_x],EBX | XCHG [L_y],EBX | XCHG [L_z],EBX | XCHG [L_a],EBX | XCHG [L_b],EBX | XCHG [L_c],EBX | XCHG [L_d],EBX | XCHG [L_e],EBX ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock05 | JE Lock11 | JE Lock17 | JE Lock23 | JE Lock29 | JE Lock35 | JE Lock41 | JE Lock47 ; Lock04: | Lock10: | Lock16: | Lock22: | Lock28: | Lock34: | Lock40: | Lock46: ; MOV EBX,[L_x] | MOV EBX,[L_y] | MOV EBX,[L_z] | MOV EBX,[L_a] | MOV EBX,[L_b] | MOV EBX,[L_c] | MOV EBX,[L_d] | MOV EBX,[L_e] ; CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 | CMP EBX,$0 ; JE Lock03 | JE Lock09 | JE Lock15 | JE Lock21 | JE Lock27 | JE Lock33 | JE Lock39 | JE Lock45 ; JMP Lock04 | JMP Lock10 | JMP Lock16 | JMP Lock22 | JMP Lock28 | JMP Lock34 | JMP Lock40 | JMP Lock46 ; Lock05: | Lock11: | Lock17: | Lock23: | Lock29: | Lock35: | Lock41: | Lock47: ; MOV EAX,[x] | MOV EAX,[y] | MOV EAX,[z] | MOV EAX,[a] | MOV EAX,[b] | MOV EAX,[c] | MOV EAX,[d] | MOV EAX,[e] ; MOV [L_x],$0 | MOV [L_y],$0 | MOV [L_z],$0 | MOV [L_a],$0 | MOV [L_b],$0 | MOV [L_c],$0 | MOV [L_d],$0 | MOV [L_e],$0 ; exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0 /\ 6:EAX=0 /\ 7:EAX=0) Generated assembler _litmus_P7_0_: cmpl $0,%edx _litmus_P7_1_: jmp Lit__L15 _litmus_P7_2_: Lit__L14: _litmus_P7_3_: LitLock42: _litmus_P7_4_: movl $1,%r12d _litmus_P7_5_: xchgl %r12d,(%r9) _litmus_P7_6_: cmpl $0,%r12d _litmus_P7_7_: je LitLock44 _litmus_P7_8_: LitLock43: _litmus_P7_9_: movl (%r9),%r12d _litmus_P7_10_: cmpl $0,%r12d _litmus_P7_11_: je LitLock42 _litmus_P7_12_: jmp LitLock43 _litmus_P7_13_: LitLock44: _litmus_P7_14_: movl $1,(%rbp) _litmus_P7_15_: movl $0,(%r9) _litmus_P7_16_: LitLock45: _litmus_P7_17_: movl $1,%r12d _litmus_P7_18_: xchgl %r12d,(%r8) _litmus_P7_19_: cmpl $0,%r12d _litmus_P7_20_: je LitLock47 _litmus_P7_21_: LitLock46: _litmus_P7_22_: movl (%r8),%r12d _litmus_P7_23_: cmpl $0,%r12d _litmus_P7_24_: je LitLock45 _litmus_P7_25_: jmp LitLock46 _litmus_P7_26_: LitLock47: _litmus_P7_27_: movl (%rdi),%eax _litmus_P7_28_: movl $0,(%r8) _litmus_P7_29_: decl %edx _litmus_P7_30_: Lit__L15: _litmus_P7_31_: jg Lit__L14 _litmus_P6_0_: cmpl $0,%edx _litmus_P6_1_: jmp Lit__L13 _litmus_P6_2_: Lit__L12: _litmus_P6_3_: LitLock36: _litmus_P6_4_: movl $1,%r12d _litmus_P6_5_: xchgl %r12d,(%r9) _litmus_P6_6_: cmpl $0,%r12d _litmus_P6_7_: je LitLock38 _litmus_P6_8_: LitLock37: _litmus_P6_9_: movl (%r9),%r12d _litmus_P6_10_: cmpl $0,%r12d _litmus_P6_11_: je LitLock36 _litmus_P6_12_: jmp LitLock37 _litmus_P6_13_: LitLock38: _litmus_P6_14_: movl $1,(%rbp) _litmus_P6_15_: movl $0,(%r9) _litmus_P6_16_: LitLock39: _litmus_P6_17_: movl $1,%r12d _litmus_P6_18_: xchgl %r12d,(%r8) _litmus_P6_19_: cmpl $0,%r12d _litmus_P6_20_: je LitLock41 _litmus_P6_21_: LitLock40: _litmus_P6_22_: movl (%r8),%r12d _litmus_P6_23_: cmpl $0,%r12d _litmus_P6_24_: je LitLock39 _litmus_P6_25_: jmp LitLock40 _litmus_P6_26_: LitLock41: _litmus_P6_27_: movl (%rdi),%eax _litmus_P6_28_: movl $0,(%r8) _litmus_P6_29_: decl %edx _litmus_P6_30_: Lit__L13: _litmus_P6_31_: jg Lit__L12 _litmus_P5_0_: cmpl $0,%edx _litmus_P5_1_: jmp Lit__L11 _litmus_P5_2_: Lit__L10: _litmus_P5_3_: LitLock30: _litmus_P5_4_: movl $1,%r12d _litmus_P5_5_: xchgl %r12d,(%r9) _litmus_P5_6_: cmpl $0,%r12d _litmus_P5_7_: je LitLock32 _litmus_P5_8_: LitLock31: _litmus_P5_9_: movl (%r9),%r12d _litmus_P5_10_: cmpl $0,%r12d _litmus_P5_11_: je LitLock30 _litmus_P5_12_: jmp LitLock31 _litmus_P5_13_: LitLock32: _litmus_P5_14_: movl $1,(%rbp) _litmus_P5_15_: movl $0,(%r9) _litmus_P5_16_: LitLock33: _litmus_P5_17_: movl $1,%r12d _litmus_P5_18_: xchgl %r12d,(%r8) _litmus_P5_19_: cmpl $0,%r12d _litmus_P5_20_: je LitLock35 _litmus_P5_21_: LitLock34: _litmus_P5_22_: movl (%r8),%r12d _litmus_P5_23_: cmpl $0,%r12d _litmus_P5_24_: je LitLock33 _litmus_P5_25_: jmp LitLock34 _litmus_P5_26_: LitLock35: _litmus_P5_27_: movl (%rdi),%eax _litmus_P5_28_: movl $0,(%r8) _litmus_P5_29_: decl %edx _litmus_P5_30_: Lit__L11: _litmus_P5_31_: jg Lit__L10 _litmus_P4_0_: cmpl $0,%edx _litmus_P4_1_: jmp Lit__L9 _litmus_P4_2_: Lit__L8: _litmus_P4_3_: LitLock24: _litmus_P4_4_: movl $1,%r12d _litmus_P4_5_: xchgl %r12d,(%r9) _litmus_P4_6_: cmpl $0,%r12d _litmus_P4_7_: je LitLock26 _litmus_P4_8_: LitLock25: _litmus_P4_9_: movl (%r9),%r12d _litmus_P4_10_: cmpl $0,%r12d _litmus_P4_11_: je LitLock24 _litmus_P4_12_: jmp LitLock25 _litmus_P4_13_: LitLock26: _litmus_P4_14_: movl $1,(%rbp) _litmus_P4_15_: movl $0,(%r9) _litmus_P4_16_: LitLock27: _litmus_P4_17_: movl $1,%r12d _litmus_P4_18_: xchgl %r12d,(%r8) _litmus_P4_19_: cmpl $0,%r12d _litmus_P4_20_: je LitLock29 _litmus_P4_21_: LitLock28: _litmus_P4_22_: movl (%r8),%r12d _litmus_P4_23_: cmpl $0,%r12d _litmus_P4_24_: je LitLock27 _litmus_P4_25_: jmp LitLock28 _litmus_P4_26_: LitLock29: _litmus_P4_27_: movl (%rdi),%eax _litmus_P4_28_: movl $0,(%r8) _litmus_P4_29_: decl %edx _litmus_P4_30_: Lit__L9: _litmus_P4_31_: jg Lit__L8 _litmus_P3_0_: cmpl $0,%edx _litmus_P3_1_: jmp Lit__L7 _litmus_P3_2_: Lit__L6: _litmus_P3_3_: LitLock18: _litmus_P3_4_: movl $1,%r12d _litmus_P3_5_: xchgl %r12d,(%r8) _litmus_P3_6_: cmpl $0,%r12d _litmus_P3_7_: je LitLock20 _litmus_P3_8_: LitLock19: _litmus_P3_9_: movl (%r8),%r12d _litmus_P3_10_: cmpl $0,%r12d _litmus_P3_11_: je LitLock18 _litmus_P3_12_: jmp LitLock19 _litmus_P3_13_: LitLock20: _litmus_P3_14_: movl $1,(%rdi) _litmus_P3_15_: movl $0,(%r8) _litmus_P3_16_: LitLock21: _litmus_P3_17_: movl $1,%r12d _litmus_P3_18_: xchgl %r12d,(%r9) _litmus_P3_19_: cmpl $0,%r12d _litmus_P3_20_: je LitLock23 _litmus_P3_21_: LitLock22: _litmus_P3_22_: movl (%r9),%r12d _litmus_P3_23_: cmpl $0,%r12d _litmus_P3_24_: je LitLock21 _litmus_P3_25_: jmp LitLock22 _litmus_P3_26_: LitLock23: _litmus_P3_27_: movl (%rbp),%eax _litmus_P3_28_: movl $0,(%r9) _litmus_P3_29_: decl %edx _litmus_P3_30_: Lit__L7: _litmus_P3_31_: jg Lit__L6 _litmus_P2_0_: cmpl $0,%edx _litmus_P2_1_: jmp Lit__L5 _litmus_P2_2_: Lit__L4: _litmus_P2_3_: LitLock12: _litmus_P2_4_: movl $1,%r12d _litmus_P2_5_: xchgl %r12d,(%r9) _litmus_P2_6_: cmpl $0,%r12d _litmus_P2_7_: je LitLock14 _litmus_P2_8_: LitLock13: _litmus_P2_9_: movl (%r9),%r12d _litmus_P2_10_: cmpl $0,%r12d _litmus_P2_11_: je LitLock12 _litmus_P2_12_: jmp LitLock13 _litmus_P2_13_: LitLock14: _litmus_P2_14_: movl $1,(%rbp) _litmus_P2_15_: movl $0,(%r9) _litmus_P2_16_: LitLock15: _litmus_P2_17_: movl $1,%r12d _litmus_P2_18_: xchgl %r12d,(%r8) _litmus_P2_19_: cmpl $0,%r12d _litmus_P2_20_: je LitLock17 _litmus_P2_21_: LitLock16: _litmus_P2_22_: movl (%r8),%r12d _litmus_P2_23_: cmpl $0,%r12d _litmus_P2_24_: je LitLock15 _litmus_P2_25_: jmp LitLock16 _litmus_P2_26_: LitLock17: _litmus_P2_27_: movl (%rdi),%eax _litmus_P2_28_: movl $0,(%r8) _litmus_P2_29_: decl %edx _litmus_P2_30_: Lit__L5: _litmus_P2_31_: jg Lit__L4 _litmus_P1_0_: cmpl $0,%edx _litmus_P1_1_: jmp Lit__L3 _litmus_P1_2_: Lit__L2: _litmus_P1_3_: LitLock06: _litmus_P1_4_: movl $1,%r12d _litmus_P1_5_: xchgl %r12d,(%r9) _litmus_P1_6_: cmpl $0,%r12d _litmus_P1_7_: je LitLock08 _litmus_P1_8_: LitLock07: _litmus_P1_9_: movl (%r9),%r12d _litmus_P1_10_: cmpl $0,%r12d _litmus_P1_11_: je LitLock06 _litmus_P1_12_: jmp LitLock07 _litmus_P1_13_: LitLock08: _litmus_P1_14_: movl $1,(%rbp) _litmus_P1_15_: movl $0,(%r9) _litmus_P1_16_: LitLock09: _litmus_P1_17_: movl $1,%r12d _litmus_P1_18_: xchgl %r12d,(%r8) _litmus_P1_19_: cmpl $0,%r12d _litmus_P1_20_: je LitLock11 _litmus_P1_21_: LitLock10: _litmus_P1_22_: movl (%r8),%r12d _litmus_P1_23_: cmpl $0,%r12d _litmus_P1_24_: je LitLock09 _litmus_P1_25_: jmp LitLock10 _litmus_P1_26_: LitLock11: _litmus_P1_27_: movl (%rdi),%eax _litmus_P1_28_: movl $0,(%r8) _litmus_P1_29_: decl %edx _litmus_P1_30_: Lit__L3: _litmus_P1_31_: jg Lit__L2 _litmus_P0_0_: cmpl $0,%edx _litmus_P0_1_: jmp Lit__L1 _litmus_P0_2_: Lit__L0: _litmus_P0_3_: LitLock00: _litmus_P0_4_: movl $1,%r12d _litmus_P0_5_: xchgl %r12d,(%r9) _litmus_P0_6_: cmpl $0,%r12d _litmus_P0_7_: je LitLock02 _litmus_P0_8_: LitLock01: _litmus_P0_9_: movl (%r9),%r12d _litmus_P0_10_: cmpl $0,%r12d _litmus_P0_11_: je LitLock00 _litmus_P0_12_: jmp LitLock01 _litmus_P0_13_: LitLock02: _litmus_P0_14_: movl $1,(%rbp) _litmus_P0_15_: movl $0,(%r9) _litmus_P0_16_: LitLock03: _litmus_P0_17_: movl $1,%r12d _litmus_P0_18_: xchgl %r12d,(%r8) _litmus_P0_19_: cmpl $0,%r12d _litmus_P0_20_: je LitLock05 _litmus_P0_21_: LitLock04: _litmus_P0_22_: movl (%r8),%r12d _litmus_P0_23_: cmpl $0,%r12d _litmus_P0_24_: je LitLock03 _litmus_P0_25_: jmp LitLock04 _litmus_P0_26_: LitLock05: _litmus_P0_27_: movl (%rdi),%eax _litmus_P0_28_: movl $0,(%r8) _litmus_P0_29_: decl %edx _litmus_P0_30_: Lit__L1: _litmus_P0_31_: jg Lit__L0 Test L08 Allowed Histogram (1 states) 1 :>0:EAX=1; 1:EAX=1; 2:EAX=1; 3:EAX=1; 4:EAX=1; 5:EAX=1; 6:EAX=1; 7:EAX=1; No Witnesses Positive: 0, Negative: 1 Condition exists (0:EAX=0 /\ 1:EAX=0 /\ 2:EAX=0 /\ 3:EAX=0 /\ 4:EAX=0 /\ 5:EAX=0 /\ 6:EAX=0 /\ 7:EAX=0) is NOT validated Hash=7d205c37ff9d35c73c5362d1f96caa7a Observation L08 Never 0 1 Time L08 88.08 Revision 6717:6722M, version 3.00+1 Parameters #ifndef SIZE_OF_TEST #define SIZE_OF_TEST 1 #endif #ifndef NUMBER_OF_RUN #define NUMBER_OF_RUN 1 #endif #ifndef AVAIL #define AVAIL 1 #endif /* gcc options: -D_GNU_SOURCE -Wall -std=gnu99 -fomit-frame-pointer -O2 -m64 -pthread */ /* barrier: user */ /* launch: fixed */ /* cache: false */ /* call: false */ /* affinity: incr0 */ /* randomise_affinity: false */ /* prealloc: false */ /* memory: direct */ /* safer: false */ /* preload: false */ /* para: self */ /* speedcheck: false */ /* proc used: 1 */ GCCOPTS="-D_GNU_SOURCE -Wall -std=gnu99 -fomit-frame-pointer -O2 -m64 -pthread" LITMUSOPTS= Tue Jan 18 15:39:37 CET 2011