A Formal Interface for Concurrent Search Structure Templates

This artifact contains the formalization accompanying the paper A Formal Interface for Concurrent Search Structure Templates. Our C implementations (in template-implementations) and the formally verified Concurrent Search Structure Templates (in template-proofs), verified using VST and flow interfaces (in flows), are included in esop26-44-artifact.tar.gz. The file templates-artifact-amd64-built.tar.gz (Apple Silicon / ARM Linux) and templates-artifact-arm64-built.tar.gz (Intel / x86_64 Linux/Windows) are Docker images containing a precompiled version of esop26-44-artifact.tar.gz, with all dependencies already installed. Detailed instructions and explanations are provided in the README.md file included in esop26-44-artifact.tar.gz. For convenience, a brief summary of the steps required to run the smoke test is also provided below. Getting Started Guide To evaluate the artifact, we provide two options: (1) using a container that has the implementation installed already (Option 1: Docker Container (Recommended)), or (2) installing the artifact locally on your machine (Option 2: Local Installation). Installation Option 1: Docker container (Recommended) To use the precompiled Docker image, first install the Docker engine. We provide two precompiled Docker images, depending on your machine architecture: Option A: AMD64 (Intel / x86_64 Linux/Windows) Use this image if you are on an Intel/AMD x86_64 machine (linux/amd64): docker load -i templates-artifact-amd64-built.tar.gz docker run --rm -it templates-artifact:amd64-built /bin/bash Option B: ARM64 (Apple Silicon / ARM Linux) Use this image if you are on Apple Silicon (M1/M2/M3/M4) or a linux/arm64 machine: docker load -i templates-artifact-arm64-built.tar.gz docker run --rm -it templates-artifact:arm64-built /bin/bash Note: Using the wrong architecture may require emulation and can be significantly slower. Installation Option 2: Local Installation (Alternative) This option builds the Rocq development locally using opam. It creates a fresh opam switch inside the artifact directory, ensuring that none of your existing Rocq/Coq developments are affected. Prerequisite This installation requires a working installation of opam. The provided script does not install opam; it only creates and uses a local switch. See opam installation instructions. Building the Artifact To build the artifact in a new opam switch, we provide an installation script, build_artifact.sh. Please run the following at the root of the artifact folder ./build_artifact.sh The ./build_artifact.sh script creates a fresh opam switch in the artifact directory, installs all required dependencies in that switch, and builds the Rocq implementation.