Vulkan-MemoryModel

The Vulkan-MemoryModel repo includes documentation and tools related to the Vulkan Memory Model that are not built into the core specification. The core specification is available at https://www.khronos.org/registry/vulkan/specs/1.1-extensions/html/vkspec.html#VK_KHR_vulkan_memory_model. Other Khronos-maintained specifications and software projects that have been extended to support this model are listed in the extension release checklist.

Alloy Model

The alloy subdirectory includes an Alloy implementation of the memory model, a set of litmus tests written in a rudimentary syntax, C++ source for a tool to translate the litmus tests to alloy, and a makefile to execute the tests. A java class to run the alloy tests is compiled against https://oss.sonatype.org/content/repositories/snapshots/org/alloytools/org.alloytools.alloy.dist/5.0.0-SNAPSHOT/org.alloytools.alloy.dist-5.0.0-20190619.101010-34.jar. Download this jar file and place it in the alloy subdirectory. Simply run "make -j4" from the alloy subdirectory to run the tests. Required dependencies are just g++, GNU make, alloy, and a Java runtime.

License

This repo is treated as an offshoot of the Vulkan-Docs repo, and uses the same Creative Commons Attribution 4.0 license. See COPYING.md.

Alloy is a third-party tool used in this repo, and is available from https://github.com/AlloyTools/org.alloytools.alloy.