Add concurrency checking based on GenMC - serial queue

.github/workflows/genmc.yaml

@@ -0,0 +1,22 @@
+# Copyright 2025, UNSW
+# SPDX-License-Identifier: BSD-2-Clause
+
+# Run genmc tests
+
+name: genmc
+
+on:
+  pull_request:
+  push:
+    branches: [ "main" ]
+
+jobs:
+  test:
+    name: Test
+    runs-on: [self-hosted, macos, ARM64]
+    steps:
+      - uses: actions/checkout@v5
+      - name: Get Nix dependencies
+        run: nix develop .#genmc -c bash -c 'echo Hello World'
+      - name: Test genmc
+        run: nix develop .#genmc --ignore-environment -c bash -c './ci/genmc/genmc.sh'

.reuse/dep5

@@ -6,6 +6,7 @@ Files:
     flake.lock
     CHANGES.md
     build.zig.zon
+    ci/genmc/nix/cmake_install.patch
     docs/design/*
     examples/i2c/build.zig.zon
     examples/serial/build.zig.zon

ci/genmc/README.md

@@ -0,0 +1,29 @@
+<!--
+    Copyright 2025, UNSW
+
+    SPDX-License-Identifier: BSD-2-Clause
+-->
+
+# GenMC
+[GenMC](https://github.com/MPI-SWS/genmc) is a model checker for verifying concurrent C programs.
+GenMC works by efficiently enumerating the state space of the concurrent system, which makes testing
+concurrent programs reliable and reproducible.
+We use it to verify partial correctness of implementations of critical concurrent data structures,
+some of our lock-free single-producer single-consumer queue, currently just the queue implementation
+used by the serial subsystem.
+
+## Usage
+Follows the instruction of GenMC to install the tool, then run
+```bash
+bash ci/genmc/genmc.sh
+```
+
+## Limitations
+GenMC does not target infinite programs. Verifying non-terminating programs under weak memory models
+is an open research problem. We also assume that the address space has been properly set up.
+
+## Trusted Computing Base
+We assume the correctness of GenMC. In addition, GenMC supports the release-acquire subset of the
+C11 memory model, which usually targets multi-threaded applications under the same address space.
+We assume the same setting applies to sddf on supported platforms, even though different protection
+domains have different address spaces.

ci/genmc/genmc.sh

@@ -0,0 +1,125 @@
+#!/bin/bash
+# Copyright 2025, UNSW
+# SPDX-License-Identifier: BSD-2-Clause
+
+cd "$(dirname "$0")/../.."
+
+set -ev
+
+for i in `seq 0 3`; do
+  export CMD="genmc --disable-estimation --disable-mm-detector --v1 -- -I./ci/genmc -I./include"
+
+  if [ $(( i % 2 )) -eq 1 ]; then
+    export CMD="$CMD -DCONFIG_ENABLE_SMP_SUPPORT=1"
+  fi
+
+  if [ $(( i / 2 )) -eq 1 ]; then
+    export CMD="$CMD -DCONFIG_DEBUG_BUILD=1"
+  fi
+
+  $CMD ./ci/genmc/serial/test1.c
+
+  $CMD -DQUEUE_SIZE=2 -DPRODUCER=2 -DCONSUMER=2 ./ci/genmc/serial/test1.c
+
+  $CMD -DQUEUE_SIZE=2 -DPRODUCER=4 -DCONSUMER=4 ./ci/genmc/serial/test1.c
+
+  $CMD -DQUEUE_SIZE=2 -DPRODUCER=6 -DCONSUMER=6 ./ci/genmc/serial/test1.c
+
+  $CMD -DQUEUE_SIZE=2 -DPRODUCER=8 -DCONSUMER=8 ./ci/genmc/serial/test1.c
+
+  $CMD -DQUEUE_SIZE=4 -DPRODUCER=4 -DCONSUMER=4 ./ci/genmc/serial/test1.c
+
+  $CMD -DQUEUE_SIZE=4 -DPRODUCER=6 -DCONSUMER=6 ./ci/genmc/serial/test1.c
+
+  $CMD -DQUEUE_SIZE=4 -DPRODUCER=7 -DCONSUMER=6 ./ci/genmc/serial/test1.c
+done
+
+for i in `seq 0 3`; do
+  export CMD="genmc --disable-estimation --disable-mm-detector --v1 -- -I./ci/genmc -I./include"
+
+  if [ $(( i % 2 )) -eq 1 ]; then
+    export CMD="$CMD -DCONFIG_ENABLE_SMP_SUPPORT=1"
+  fi
+
+  if [ $(( i / 2 )) -eq 1 ]; then
+    export CMD="$CMD -DCONFIG_DEBUG_BUILD=1"
+  fi
+
+  $CMD ./ci/genmc/serial/test2.c
+
+  $CMD -DQUEUE_SIZE=2 -DPRODUCER=2 -DCONSUMER=2 -DBATCH_SIZE=1 ./ci/genmc/serial/test2.c
+
+  $CMD -DQUEUE_SIZE=2 -DPRODUCER=2 -DCONSUMER=2 -DBATCH_SIZE=2 ./ci/genmc/serial/test2.c
+
+  $CMD -DQUEUE_SIZE=2 -DPRODUCER=4 -DCONSUMER=4 -DBATCH_SIZE=1 ./ci/genmc/serial/test2.c
+
+  $CMD -DQUEUE_SIZE=2 -DPRODUCER=4 -DCONSUMER=4 -DBATCH_SIZE=2 ./ci/genmc/serial/test2.c
+
+  $CMD -DQUEUE_SIZE=2 -DPRODUCER=6 -DCONSUMER=6 -DBATCH_SIZE=1 ./ci/genmc/serial/test2.c
+
+  $CMD -DQUEUE_SIZE=2 -DPRODUCER=6 -DCONSUMER=6 -DBATCH_SIZE=2 ./ci/genmc/serial/test2.c
+
+  $CMD -DQUEUE_SIZE=2 -DPRODUCER=8 -DCONSUMER=8 -DBATCH_SIZE=1 ./ci/genmc/serial/test2.c
+
+  $CMD -DQUEUE_SIZE=2 -DPRODUCER=8 -DCONSUMER=8 -DBATCH_SIZE=2 ./ci/genmc/serial/test2.c
+
+  $CMD -DQUEUE_SIZE=4 -DPRODUCER=4 -DCONSUMER=4 -DBATCH_SIZE=1 ./ci/genmc/serial/test2.c
+
+  $CMD -DQUEUE_SIZE=4 -DPRODUCER=4 -DCONSUMER=4 -DBATCH_SIZE=2 ./ci/genmc/serial/test2.c
+
+  $CMD -DQUEUE_SIZE=4 -DPRODUCER=4 -DCONSUMER=4 -DBATCH_SIZE=3 ./ci/genmc/serial/test2.c
+
+  $CMD -DQUEUE_SIZE=4 -DPRODUCER=4 -DCONSUMER=4 -DBATCH_SIZE=4 ./ci/genmc/serial/test2.c
+
+  $CMD -DQUEUE_SIZE=4 -DPRODUCER=6 -DCONSUMER=6 -DBATCH_SIZE=3 ./ci/genmc/serial/test2.c
+
+  $CMD -DQUEUE_SIZE=4 -DPRODUCER=6 -DCONSUMER=6 -DBATCH_SIZE=4 ./ci/genmc/serial/test2.c
+
+  $CMD -DQUEUE_SIZE=4 -DPRODUCER=7 -DCONSUMER=6 -DBATCH_SIZE=3 ./ci/genmc/serial/test2.c
+
+  $CMD -DQUEUE_SIZE=4 -DPRODUCER=7 -DCONSUMER=6 -DBATCH_SIZE=4 ./ci/genmc/serial/test2.c
+done
+
+for i in `seq 0 3`; do
+  export CMD="genmc --disable-estimation --disable-mm-detector --v1 -- -I./ci/genmc -I./include"
+
+  if [ $(( i % 2 )) -eq 1 ]; then
+    export CMD="$CMD -DCONFIG_ENABLE_SMP_SUPPORT=1"
+  fi
+
+  if [ $(( i / 2 )) -eq 1 ]; then
+    export CMD="$CMD -DCONFIG_DEBUG_BUILD=1"
+  fi
+
+  $CMD ./ci/genmc/serial/test3.c
+
+  $CMD -DQUEUE_SIZE=2 -DPRODUCER=2 -DCONSUMER=2 -DBATCH_SIZE=1 ./ci/genmc/serial/test3.c
+
+  $CMD -DQUEUE_SIZE=2 -DPRODUCER=4 -DCONSUMER=2 -DBATCH_SIZE=2 ./ci/genmc/serial/test3.c
+
+  $CMD -DQUEUE_SIZE=2 -DPRODUCER=4 -DCONSUMER=4 -DBATCH_SIZE=1 ./ci/genmc/serial/test3.c
+
+  $CMD -DQUEUE_SIZE=2 -DPRODUCER=6 -DCONSUMER=6 -DBATCH_SIZE=1 ./ci/genmc/serial/test3.c
+
+  $CMD -DQUEUE_SIZE=2 -DPRODUCER=6 -DCONSUMER=3 -DBATCH_SIZE=2 ./ci/genmc/serial/test3.c
+
+  $CMD -DQUEUE_SIZE=2 -DPRODUCER=8 -DCONSUMER=8 -DBATCH_SIZE=1 ./ci/genmc/serial/test3.c
+
+  $CMD -DQUEUE_SIZE=2 -DPRODUCER=8 -DCONSUMER=4 -DBATCH_SIZE=2 ./ci/genmc/serial/test3.c
+
+  $CMD -DQUEUE_SIZE=4 -DPRODUCER=4 -DCONSUMER=4 -DBATCH_SIZE=1 ./ci/genmc/serial/test3.c
+
+  $CMD -DQUEUE_SIZE=4 -DPRODUCER=4 -DCONSUMER=2 -DBATCH_SIZE=2 ./ci/genmc/serial/test3.c
+
+  $CMD -DQUEUE_SIZE=4 -DPRODUCER=4 -DCONSUMER=1 -DBATCH_SIZE=3 ./ci/genmc/serial/test3.c
+
+  $CMD -DQUEUE_SIZE=4 -DPRODUCER=4 -DCONSUMER=1 -DBATCH_SIZE=4 ./ci/genmc/serial/test3.c
+
+  $CMD -DQUEUE_SIZE=4 -DPRODUCER=6 -DCONSUMER=2 -DBATCH_SIZE=3 ./ci/genmc/serial/test3.c
+
+  $CMD -DQUEUE_SIZE=4 -DPRODUCER=6 -DCONSUMER=1 -DBATCH_SIZE=4 ./ci/genmc/serial/test3.c
+
+  $CMD -DQUEUE_SIZE=4 -DPRODUCER=7 -DCONSUMER=2 -DBATCH_SIZE=3 ./ci/genmc/serial/test3.c
+
+  $CMD -DQUEUE_SIZE=4 -DPRODUCER=7 -DCONSUMER=1 -DBATCH_SIZE=4 ./ci/genmc/serial/test3.c
+done

ci/genmc/nix/cmake_install.patch

@@ -0,0 +1,25 @@
+diff --git a/CMakeLists.txt b/CMakeLists.txt
+index 9ef8718..d4b474a 100644
+--- a/CMakeLists.txt
++++ b/CMakeLists.txt
+@@ -12,7 +12,7 @@ set(PACKAGE_NAME "GenMC")
+ set(PACKAGE_BUGREPORT "michalis.kokologiannakis@inf.ethz.ch")
+ set(PACKAGE_URL "https://plv.mpi-sws.org/genmc")
+ set(PACKAGE_VERSION "${CMAKE_PROJECT_VERSION}")
+-set(INCLUDE_DIR "${CMAKE_INSTALL_PREFIX}/${PKG_INCLUDE_DIR}")
++set(INCLUDE_DIR "${PKG_INCLUDE_DIR}")
+ set(SRC_INCLUDE_DIR "${CMAKE_SOURCE_DIR}/include")
+ set(RUST_DIR "${CMAKE_SOURCE_DIR}/rust")
+
+diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
+index 5bb5c05..227c189 100644
+--- a/src/CMakeLists.txt
++++ b/src/CMakeLists.txt
+@@ -104,7 +104,7 @@ endif()
+
+ ### GenMC executable
+ add_executable(${PROJECT_NAME} main.cpp)
+-install(TARGETS ${PROJECT_NAME} RUNTIME DESTINATION ${CMAKE_INSTALL_BINDIR}/${PROJECT_NAME})
++install(TARGETS ${PROJECT_NAME} RUNTIME)
+
+ target_link_libraries(${PROJECT_NAME} PRIVATE genmc_config_includes genmc_lib)

ci/genmc/nix/package.nix

@@ -0,0 +1,48 @@
+#
+# Copyright 2025, UNSW
+# SPDX-License-Identifier: BSD-2-Clause
+#
+{
+  fetchFromGitHub,
+  stdenv,
+  lib,
+  llvm,
+  clang,
+  clang-complete,
+  cmake,
+  pkg-config,
+  libxml2,
+  libffi,
+}:
+stdenv.mkDerivation (rec {
+  pname = "genmc";
+  version = "v0.13.0";
+  src = fetchFromGitHub {
+    owner = "MPI-SWS";
+    repo = "genmc";
+    rev = version;
+    hash = "sha256-a+ZhzuKmhLem8ScCKI1EW8KTy+UuhmzU1Vt8y+NzS8c=";
+  };
+
+  nativeBuildInputs = [
+    cmake
+    libxml2
+    pkg-config
+    llvm
+    clang
+    libffi
+  ];
+
+  buildInputs = [
+    clang-complete
+  ];
+
+  cmakeFlags = [
+    "-DLLVM_CONFIG_PATH=llvm-config"
+    "-DCLANGPATH=${lib.getExe clang-complete}"
+  ];
+
+  patches = [
+    ./cmake_install.patch
+  ];
+})

ci/genmc/os/sddf.h

@@ -0,0 +1,7 @@
+/*
+ * Copyright 2025, UNSW
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+/* This is a fake header file for GenMC model checking. */

ci/genmc/serial/test1.c

@@ -0,0 +1,80 @@
+/*
+ * Copyright 2025, UNSW
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+#include <assert.h>
+#include <stdlib.h>
+#include <pthread.h>
+
+#include <sddf/serial/queue.h>
+
+#ifndef QUEUE_SIZE
+#define QUEUE_SIZE 1
+#endif
+
+#ifndef PRODUCER
+#define PRODUCER 1
+#endif
+
+#ifndef CONSUMER
+#define CONSUMER 1
+#endif
+
+#if PRODUCER < CONSUMER
+#error "the producer size must be not less than the consumer size"
+#endif
+
+static serial_queue_handle_t queue_handle;
+
+void *producer(void *p)
+{
+    for (uint64_t i = 0; i < PRODUCER; i++) {
+        while (serial_enqueue(&queue_handle, (char)i) != 0);
+    }
+    return NULL;
+}
+
+void *consumer(void *p)
+{
+    for (uint64_t i = 0; i < CONSUMER; i++) {
+        char character;
+        while (serial_dequeue(&queue_handle, &character) != 0);
+        assert(character == (char)i);
+    }
+    return NULL;
+}
+
+int main()
+{
+    serial_queue_t *queue = malloc(sizeof(serial_queue_t));
+    if (queue == NULL) {
+        exit(1);
+    }
+    queue->tail = 0;
+    queue->head = 0;
+    queue->producer_signalled = 0;
+
+    char *data_region = malloc(QUEUE_SIZE * sizeof(char));
+    if (data_region == NULL) {
+        exit(1);
+    }
+
+    serial_queue_init(&queue_handle, queue, QUEUE_SIZE, data_region);
+
+    pthread_t t1, t2;
+    if (pthread_create(&t1, NULL, producer, NULL) != 0) {
+        exit(1);
+    }
+    if (pthread_create(&t2, NULL, consumer, NULL) != 0) {
+        exit(1);
+    }
+
+    pthread_join(t2, NULL);
+    pthread_join(t1, NULL);
+
+    free(data_region);
+    free(queue);
+
+    return 0;
+}