GPU_PTX sl_future-p0::p1-xgyg {y=1;} P0 | P1 ; ld.cg.u32 r0, [r1] | atom.cas.b32 r0, [r1], 0, 1 ; mov.u32 r2, 0 | mov.u32 r2, 1 ; st.cg.u32 [r3], r2 | setp.eq.u32 r4, r0, 0 ; membar.gl | @r4 mov.u32 r5, 1 ; | @r4 st.cg.u32 [r3], r2 ; exists (0:r0=1 /\ 1:r0=0) (device (kernel (cta (warp P0)) (cta (warp P1)))) y:global; x:global Generated assembler //START _litmus_P1 atom.cas.b32 sr01, [sr11], 0, 1 ; mov.u32 sr21, 1 ; setp.eq.u32 sr41, sr01, 0 ; @sr41 mov.u32 sr51, 1 ; @sr41 st.cg.u32 [sr31], sr21 ; //START _litmus_P0 ld.cg.u32 sr00, [sr10] ; mov.u32 sr20, 0 ; st.cg.u32 [sr30], sr20 ; membar.gl ; Binary '/tmp/dird96979.tmp/sl-future.exe' successfully loaded Specification clusters: 2 Specification: [[(818, 6, 'R4'), (822, 2, 'R10')], [(863, 3, 'R4'), (866, 2, 'R10')]] Cluster 0: OK Cluster 1: OK !!SUCCESS!! Test sl-future Allowed Histogram (3 states) 60212 :>0:r0=0; 1:r0=0; 58 *>0:r0=1; 1:r0=0; 39735 :>0:r0=0; 1:r0=1; Ok Witnesses Positive: 58, Negative: 99947 Condition exists (0:r0=1 /\ 1:r0=0) is validated Observation sl-future Sometimes 58 99947 Time sl-future 6.21 -- device info -- Name: GeForce GTX TITAN Major revision number: 3 Minor revision number: 5 Total global memory: 6442123264 Total shared memory per block: 49152 Number of multiprocessors: 14 Machine: formal Revision 1371, version 5.01 GPU_PTX experimental backend Command line: ./litmus -mach GTXTitan.cfg -gpu-verf-comp true ASPLOS/sl-future.litmus -gpu-general-bc false Parameters #ifndef SIZE_OF_TEST #define SIZE_OF_TEST 100000 #endif #ifndef NUMBER_OF_RUN #define NUMBER_OF_RUN 1 #endif /* cc options: -arch=sm_35 */ /* barrier: user */ /* speedcheck: no */ /* gpu_general_bc: false */ /* gpu_mem_stress: true */ /* gpu-rand-threads: true */ /* gpu_cuda: true */ /* gpu_gen_addr: true */ /* gpu_cvt_global_to_gen: true */ /* gpu_cvt_shared_to_gen: true */ /* gpu_max_ctas: 14 */ /* gpu_min_ctas: 10 */ /* gpu_max_threads: 512 */ /* gpu_min_threads: 128 */