Add concurrency checking based on GenMC

.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

benchmark/benchmark.c

@@ -15,17 +15,6 @@
 #include <sddf/util/util.h>
 #include <sddf/util/printf.h>
 
-/* At the moment we run systems that contain this benchmarking code on architectures
- * where we cannot properly do benchmarking. We also include the benchmarking PD
- * on non-benchmarking configurations.
- * This defines whether we actually try to benchmark, setup the PMU etc.
- */
-#if defined(CONFIG_ENABLE_BENCHMARKS) && defined(CONFIG_ARCH_ARM)
-#define ENABLE_BENCHMARKING 1
-#else
-#define ENABLE_BENCHMARKING 0
-#endif
-
 #define LOG_BUFFER_CAP 7
 
 __attribute__((__section__(".benchmark_config"))) benchmark_config_t benchmark_config;

benchmark/idle.c

@@ -20,7 +20,7 @@ struct bench *b;
 
 void count_idle(void)
 {
-#if defined(MICROKIT_CONFIG_benchmark) && defined(CONFIG_ARCH_ARM)
+#if ENABLE_BENCHMARKING
     uint64_t val;
     SEL4BENCH_READ_CCNT(val);
     b->prev = val;

ci/genmc/README.md

@@ -0,0 +1,28 @@
+<!--
+    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,
+including the lock-free single-producer single-consumer queue.
+
+## 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,37 @@
+#!/bin/bash
+# Copyright 2025, UNSW
+# SPDX-License-Identifier: BSD-2-Clause
+
+cd "$(dirname "$0")/../.."
+
+set -ev
+
+for i in `seq 0 1`; do
+  export CMD="genmc --disable-estimation --disable-mm-detector --v1 -- -I./ci/genmc -I./include"
+
+  if [ "$i" -eq 1 ]; then
+    export CMD="$CMD -DCONFIG_ENABLE_SMP_SUPPORT=1"
+  fi
+
+  $CMD ./ci/genmc/network/test1.c
+
+  $CMD -DQUEUE_SIZE=2 -DPRODUCER=2 -DCONSUMER=2 ./ci/genmc/network/test1.c
+
+  $CMD -DQUEUE_SIZE=2 -DPRODUCER=4 -DCONSUMER=4 ./ci/genmc/network/test1.c
+
+  $CMD -DQUEUE_SIZE=2 -DPRODUCER=6 -DCONSUMER=6 ./ci/genmc/network/test1.c
+
+  $CMD -DQUEUE_SIZE=2 -DPRODUCER=8 -DCONSUMER=8 ./ci/genmc/network/test1.c
+
+  $CMD -DQUEUE_SIZE=3 -DPRODUCER=4 -DCONSUMER=4 ./ci/genmc/network/test1.c
+
+  $CMD -DQUEUE_SIZE=3 -DPRODUCER=6 -DCONSUMER=6 ./ci/genmc/network/test1.c
+
+  $CMD -DQUEUE_SIZE=3 -DPRODUCER=7 -DCONSUMER=7 ./ci/genmc/network/test1.c
+
+  $CMD -DQUEUE_SIZE=4 -DPRODUCER=4 -DCONSUMER=4 ./ci/genmc/network/test1.c
+
+  $CMD -DQUEUE_SIZE=4 -DPRODUCER=6 -DCONSUMER=6 ./ci/genmc/network/test1.c
+
+  $CMD -DQUEUE_SIZE=4 -DPRODUCER=7 -DCONSUMER=6 ./ci/genmc/network/test1.c
+done

ci/genmc/network/test1.c

@@ -0,0 +1,85 @@
+/*
+ * Copyright 2025, UNSW
+ * SPDX-License-Identifier: BSD-2-Clause
+ */
+
+#include <assert.h>
+#include <stdlib.h>
+#include <pthread.h>
+
+#include <sddf/network/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
+
+net_queue_handle_t queue;
+
+void *producer(void *p)
+{
+    for (uint64_t i = 0; i < PRODUCER; i++) {
+        net_buff_desc_t desc = { 0 };
+        desc.io_or_offset = i;
+        while (net_enqueue_free(&queue, desc) != 0);
+    }
+    return NULL;
+}
+
+void *consumer(void *p)
+{
+    for (uint64_t i = 0; i < CONSUMER; i++) {
+        net_buff_desc_t desc;
+        while (net_dequeue_free(&queue, &desc) != 0);
+        assert(desc.io_or_offset == i);
+    }
+    return NULL;
+}
+
+int main()
+{
+    net_queue_t *free_queue = malloc(sizeof(net_queue_t) + sizeof(net_buff_desc_t) * QUEUE_SIZE);
+    if (free_queue == NULL) {
+        exit(1);
+    }
+    free_queue->head = 0;
+    free_queue->tail = 0;
+    free_queue->consumer_signalled = 0;
+
+    net_queue_t *active_queue = malloc(sizeof(net_queue_t) + sizeof(net_buff_desc_t) * QUEUE_SIZE);
+    if (active_queue == NULL) {
+        exit(1);
+    }
+    active_queue->head = 0;
+    active_queue->tail = 0;
+    active_queue->consumer_signalled = 0;
+
+    net_queue_init(&queue, free_queue, active_queue, QUEUE_SIZE);
+
+    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(active_queue);
+    free(free_queue);
+
+    return 0;
+}

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
+  ];
+})

flake.nix

@@ -47,11 +47,41 @@
             pythonPackages = pkgs.python312Packages;
           };
 
+          clang-complete = (pkgs.symlinkJoin {
+            name = "clang-complete";
+            paths = llvm.clang-unwrapped.all;
+            meta.mainProgram = "clang";
+
+            # Clang searches up from the directory where it sits to find its built-in
+            # headers. The `symlinkJoin` creates a symlink to the clang binary, and that
+            # symlink is what ends up in your PATH from this shell. However, that symlink's
+            # destination, the clang binary file, still resides in its own nix store
+            # entry (`llvm.clang-unwrapped`), isolated from the header files (found in
+            # `llvm.clang-unwrapped.lib` under `lib/clang/18/include`). So when search up its
+            # parent directories, no built-in headers are found.
+            #
+            # By copying over the clang binary over the symlinks in the realisation of the
+            # `symlinkJoin`, we can fix this; now the search mechanism looks up the parent
+            # directories of the `clang` binary (which is a copy created by below command),
+            # until it finds the aforementioned `lib/clang/18/include` (where the `lib` is
+            # actually a symlink to `llvm.clang-unwrapped.lib + "/lib"`).
+            postBuild = ''
+              cp --remove-destination -- ${llvm.clang-unwrapped}/bin/* $out/bin/
+            '';
+          });
+
+          genmc = pkgs.callPackage ./ci/genmc/nix/package.nix { inherit clang-complete; llvm = pkgs.llvmPackages_20.llvm; };
+
           pythonTool = pkgs.python312.withPackages (ps: [
             pysdfgen
           ]);
         in
         {
+          genmc = pkgs.mkShell rec {
+            nativeBuildInputs = [
+              genmc
+            ];
+          };
 
           # For building the design documnet
           docs = pkgs.mkShell rec {
@@ -93,29 +123,7 @@
               perl
               which
               gptfdisk
-
-              (symlinkJoin {
-                name = "clang-complete";
-                paths = llvm.clang-unwrapped.all;
-
-                # Clang searches up from the directory where it sits to find its built-in
-                # headers. The `symlinkJoin` creates a symlink to the clang binary, and that
-                # symlink is what ends up in your PATH from this shell. However, that symlink's
-                # destination, the clang binary file, still resides in its own nix store
-                # entry (`llvm.clang-unwrapped`), isolated from the header files (found in
-                # `llvm.clang-unwrapped.lib` under `lib/clang/18/include`). So when search up its
-                # parent directories, no built-in headers are found.
-                #
-                # By copying over the clang binary over the symlinks in the realisation of the
-                # `symlinkJoin`, we can fix this; now the search mechanism looks up the parent
-                # directories of the `clang` binary (which is a copy created by below command),
-                # until it finds the aforementioned `lib/clang/18/include` (where the `lib` is
-                # actually a symlink to `llvm.clang-unwrapped.lib + "/lib"`).
-                postBuild = ''
-                  cp --remove-destination -- ${llvm.clang-unwrapped}/bin/* $out/bin/
-                '';
-              })
-
+              clang-complete
               # for git-clang-format.
               llvm.libclang.python
               llvm.lld

include/sddf/benchmark/config.h

@@ -8,6 +8,17 @@
 #include <os/sddf.h>
 #include <stdint.h>
 
+/* At the moment we run systems that contain this benchmarking code on architectures
+ * where we cannot properly do benchmarking. We also include the benchmarking PD
+ * on non-benchmarking configurations.
+ * This defines whether we actually try to benchmark, setup the PMU etc.
+ */
+#if defined(CONFIG_ENABLE_BENCHMARKS) && defined(CONFIG_ARCH_ARM)
+#define ENABLE_BENCHMARKING 1
+#else
+#define ENABLE_BENCHMARKING 0
+#endif
+
 #define BENCHMARK_MAX_CHILDREN 64 // TODO: Can we have a higher upper bound on this?
 
 typedef struct benchmark_child_config {