This artifact accompanies the paper "Towards Unified Analysis of GPU Consistency" by Haining Tong, Natalia Gavrilenko, Hernán Ponce de León, and Keijo Heljanko. It contains a Dockerfile that installs all tools, scrips, and data required to reproduce the experiments in the paper.
Building a docker image:
docker build . -t dat3m-gpu-artifact
Running a docker container:
docker run -ti --rm dat3m-gpu-artifact
Commands:
python3 /home/scripts/generate-table-3.py
python3 /home/scripts/generate-table-4.py
python3 /home/scripts/generate-table-5.py
python3 /home/scripts/generate-plots.py
Running a litmus test with dartagnan
Command:
cd /home/Dat3M && java -jar dartagnan/target/dartagnan.jar \
<path/to/test.litmus> \
<cat/ptx-v6.0.cat|cat/ptx-v7.5.cat|cat/spirv.cat> \
--property=<program_spec|cat_spec|liveness> \
--target=<ptx|vulkan> \
--method=assume
Example:
cd /home/Dat3M && java -jar dartagnan/target/dartagnan.jar \
litmus/PTX/Manual/MP-gpu.litmus \
cat/ptx-v7.5.cat \
--property=program_spec \
--target=ptx \
--method=assume
cd /home/Dat3M && java -jar dartagnan/target/dartagnan.jar \
litmus/VULKAN/Data-Race/mp-filter.litmus \
cat/spirv.cat \
--property=cat_spec \
--target=vulkan \
--method=assume
cd /home/Dat3M && java -jar dartagnan/target/dartagnan.jar \
litmus/VULKAN/CADP/2_threads_2_instructions/4_simple.litmus \
cat/spirv.cat \
--property=liveness \
--target=vulkan \
--method=assume
Options:
<path/to/test.litmus>
path to a litmus test file<cat/ptx-v6.0.cat|cat/ptx-v7.5.cat|cat/spirv.cat>
path to a consistency model filecat/ptx-v6.0.cat
ptx model v6.0 (for ptx tests)cat/ptx-v7.5.cat
ptx model v7.5 (for ptx tests)cat/spirv.cat
vulkan model (for vulkan tests)
property=<program_spec|cat_spec|liveness>
verification propertyprogram_spec
assertions on final state (default)cat_spec
data-race freedomliveness
termination guarantees
target=<ptx|vulkan>
target architecture (must agree with test type)ptx
for ptx testsvulkan
for vulkan tests
Tests:
/home/Dat3M/litmus/PTX
/home/Dat3M/litmus/VULKAN
/home/benchmarks/dat3m_ptx
/home/benchmarks/dat3m_vkn
Running a spirv test with dartagnan
Command:
cd /home/Dat3M && java -jar dartagnan/target/dartagnan.jar \
<path/to/test.spv.dis> \
cat/spirv.cat \
--property=<program_spec|cat_spec|liveness> \
--bound=<loop-bound> \
--target=vulkan \
--encoding.integers=true \
--method=assume
Example:
cd /home/Dat3M && java -jar dartagnan/target/dartagnan.jar \
/home/benchmarks/spirv/xf-barrier-9.spv.dis \
cat/spirv.cat \
--property=cat_spec \
--target=vulkan \
--bound=9 \
--encoding.integers=true \
--method=assume
Options:
<path/to/test.spv.dis>
path to a test fileproperty=<program_spec|cat_spec|liveness>
verification propertyprogram_spec
assertions on final state (default)cat_spec
data-race freedomliveness
termination guarantees
bound=<loop-bound>
unrolling bound for all loops (default 1)
Tests:
/home/Dat3M/dartagnan/src/test/resources/spirv
/home/benchmarks/spirv
Running a ptx test with alloy
Command:
cd /home/mixedproxy && src/test_to_alloy.py <path/to/test.test>
Example:
cd /home/mixedproxy && src/test_to_alloy.py /home/mixedproxy/tests/MP_gpu.test
Tests:
/home/mixedproxy/tests
/home/benchmarks/alloy_ptx
Running a vulkan test with alloy
Command:
cd /home/Vulkan-MemoryModel/alloy && \
java -cp "org.alloytools.alloy.dist-5.0.0-20190619.101010-34.jar:." \
RunCommandLine <path/to/test.test.gen>
Example:
cd /home/Vulkan-MemoryModel/alloy && \
java -cp "org.alloytools.alloy.dist-5.0.0-20190619.101010-34.jar:." \
RunCommandLine /home/Vulkan-MemoryModel/alloy/build/mp.test.gen
Tests:
/home/Vulkan-MemoryModel/alloy/build
/home/benchmarks/alloy_vkn
Running an opencl test with gpuverify
Command:
python3 /home/gpuverify-release/GPUVerify.py \
--local_size=<local-size> \
--global_size=<global-size> \
--no-benign-tolerance \
<path/to/test.cl>
Example:
python3 /home/gpuverify-release/GPUVerify.py \
--local_size=1024 \
--global_size=2048 \
--no-benign-tolerance \
/home/Dat3M/benchmarks/opencl/caslock-gpu-verify.cl
Options:
<local-size>
number of threads in workgroup<global-size>
total number of threads (should be a multiple oflocal-size
)<path/to/test.cl>
path to the test file
Tests:
/home/gpuverify-release/testsuite/OpenCL
/home/Dat3M/benchmarks/opencl/
Compiling and disassembling opencl kernels
Command:
clspv <path/to/test.cl> \
--cl-std=CL2.0 --inline-entry-points \
--spv-version=1.6 -o kernel.spv
spirv-dis kernel.spv > kernel.spv.dis
rm kernel.spv
Example:
clspv /home/Dat3M/benchmarks/opencl/xf-barrier.cl \
--cl-std=CL2.0 --inline-entry-points \
--spv-version=1.6 -o kernel.spv
spirv-dis kernel.spv > kernel.spv.dis
rm kernel.spv
Tests:
/home/gpuverify-release/testsuite/OpenCL
/home/Dat3M/benchmarks/opencl
Generating test configuration: In addition to the spirv code itself, dartagnan expects the configuration of the test as part of its input. This configuration is given as a comment at the top of a disassembled spirv file and should be generated manually. Dartagnan expects the following configuration parameters:
@Config (x, y, z)
threads hierarchy (default 1, 1, 1)x
the number of threads in a subgroupy
the number of subgroups in a workgroupz
the number of workgroups in a queue family
@Input
values normally passed from a host to a device via a shared buffer (mandatory for runtime array variable type)@Output
assertions on the output values (mandatory forprogram_spec
verification property)
Example:
; @Input: %17 = {{0}}
; @Input: %18 = {{0}}
; @Input: %19 = {{-1, -1}}
; @Output: forall (%19[0][0] != %19[0][1])
; @Config: 4, 1, 2