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/dire776fe.tmp/sl-future.exe' successfully loaded Specification clusters: 2 Specification: [[(502, 6, 'R4'), (506, 2, 'R12')], [(549, 3, 'R4'), (553, 2, 'R12')]] Cluster 0: OK Cluster 1: OK !!SUCCESS!! Test sl-future Allowed Histogram (3 states) 59043 :>0:r0=0; 1:r0=0; 41 *>0:r0=1; 1:r0=0; 40916 :>0:r0=0; 1:r0=1; Ok Witnesses Positive: 41, Negative: 99959 Condition exists (0:r0=1 /\ 1:r0=0) is validated Observation sl-future Sometimes 41 99959 Time sl-future 7.02 -- device info -- Name: GeForce GTX 660 Major revision number: 3 Minor revision number: 0 Total global memory: 2147155968 Total shared memory per block: 49152 Number of multiprocessors: 5 Machine: csu8975 Revision 1398M, version 5.01 GPU_PTX experimental backend Command line: ./litmus -mach GTX660.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_30 */ /* 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: 5 */ /* gpu_min_ctas: 4 */ /* gpu_max_threads: 256 */ /* gpu_min_threads: 128 */