diff --git a/.github/workflows/genmc.yaml b/.github/workflows/genmc.yaml new file mode 100644 index 000000000..0ad8c592d --- /dev/null +++ b/.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' diff --git a/.reuse/dep5 b/.reuse/dep5 index cbab57da7..ae4c5212b 100644 --- a/.reuse/dep5 +++ b/.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 diff --git a/ci/genmc/README.md b/ci/genmc/README.md new file mode 100644 index 000000000..dd5d5fb61 --- /dev/null +++ b/ci/genmc/README.md @@ -0,0 +1,29 @@ + + +# 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. diff --git a/ci/genmc/genmc.sh b/ci/genmc/genmc.sh new file mode 100755 index 000000000..f32726dbe --- /dev/null +++ b/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 diff --git a/ci/genmc/nix/cmake_install.patch b/ci/genmc/nix/cmake_install.patch new file mode 100644 index 000000000..f70906981 --- /dev/null +++ b/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) diff --git a/ci/genmc/nix/package.nix b/ci/genmc/nix/package.nix new file mode 100644 index 000000000..ef18887f1 --- /dev/null +++ b/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 + ]; +}) diff --git a/ci/genmc/os/sddf.h b/ci/genmc/os/sddf.h new file mode 100644 index 000000000..90bc2b336 --- /dev/null +++ b/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. */ diff --git a/ci/genmc/serial/test1.c b/ci/genmc/serial/test1.c new file mode 100644 index 000000000..e5b602c90 --- /dev/null +++ b/ci/genmc/serial/test1.c @@ -0,0 +1,80 @@ +/* + * Copyright 2025, UNSW + * SPDX-License-Identifier: BSD-2-Clause + */ + +#include +#include +#include + +#include + +#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; +} diff --git a/ci/genmc/serial/test2.c b/ci/genmc/serial/test2.c new file mode 100644 index 000000000..78a6e7605 --- /dev/null +++ b/ci/genmc/serial/test2.c @@ -0,0 +1,92 @@ +/* + * Copyright 2025, UNSW + * SPDX-License-Identifier: BSD-2-Clause + */ + +#include +#include +#include + +#include + +#ifndef QUEUE_SIZE +#define QUEUE_SIZE 1 +#endif + +#ifndef PRODUCER +#define PRODUCER 1 +#endif + +#ifndef CONSUMER +#define CONSUMER 1 +#endif + +#ifndef BATCH_SIZE +#define BATCH_SIZE 1 +#endif + +#if PRODUCER * BATCH_SIZE < CONSUMER +#error "the producer size must be not less than the consumer size" +#endif + +#if QUEUE_SIZE < BATCH_SIZE +#error "the queue size must be not less than the batch size" +#endif + +static serial_queue_handle_t queue_handle; + +void *producer(void *p) +{ + uint32_t local_tail = 0; + for (uint64_t i = 0; i < PRODUCER; i++) { + for (uint64_t j = 0; j < BATCH_SIZE; j++) { + while (serial_enqueue_local(&queue_handle, &local_tail, (char)(i * BATCH_SIZE + j)) != 0); + } + serial_update_shared_tail(&queue_handle, local_tail); + } + 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; +} diff --git a/ci/genmc/serial/test3.c b/ci/genmc/serial/test3.c new file mode 100644 index 000000000..cde490d3e --- /dev/null +++ b/ci/genmc/serial/test3.c @@ -0,0 +1,91 @@ +/* + * Copyright 2025, UNSW + * SPDX-License-Identifier: BSD-2-Clause + */ + +#include +#include +#include + +#include + +#ifndef QUEUE_SIZE +#define QUEUE_SIZE 1 +#endif + +#ifndef PRODUCER +#define PRODUCER 1 +#endif + +#ifndef CONSUMER +#define CONSUMER 1 +#endif + +#ifndef BATCH_SIZE +#define BATCH_SIZE 1 +#endif + +#if PRODUCER < CONSUMER * BATCH_SIZE +#error "the producer size must be not less than the consumer size" +#endif + +#if QUEUE_SIZE < BATCH_SIZE +#error "the queue size must be not less than the batch 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) +{ + uint32_t local_head = 0; + for (uint64_t i = 0; i < CONSUMER; i++) { + for (uint64_t j = 0; j < BATCH_SIZE; j++) { + char character; + while (serial_dequeue_local(&queue_handle, &local_head, &character) != 0); + assert(character == (char)(i * BATCH_SIZE + j)); + } + } + 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; +} diff --git a/flake.nix b/flake.nix index fc9053a4f..de9ffb45c 100644 --- a/flake.nix +++ b/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 diff --git a/include/sddf/serial/queue.h b/include/sddf/serial/queue.h index 57efca721..3e876e2f6 100644 --- a/include/sddf/serial/queue.h +++ b/include/sddf/serial/queue.h @@ -13,6 +13,15 @@ #include #include +/** + * The serial queue, like all sDDF queues, is an implementation of a single-producer, + * single-consumer FIFO queue. The key assumption being that only the producer is permitted to + * modify the tail, and only the consumer is permitted to modify the head. Both components are + * permitted to read both indices. The library's atomic operations are written to ensure correctness + * under these assumptions, thus each function's description contains an explicit notes on its + * assumed caller. + */ + typedef struct serial_queue { /* index to insert at */ uint32_t tail; @@ -29,46 +38,90 @@ typedef struct serial_queue_handle { } serial_queue_handle_t; /** - * Return the number of bytes of data stored in the queue. + * Return the number of bytes of data stored in the queue. This is calculated by + * using the head and tail values currently stored in the shared queue handle + * data structure. This function should only be called by the CONSUMER of the + * queue. * * @param queue_handle queue containing the data. * * @return The number bytes of data stored in the queue. */ -static inline uint32_t serial_queue_length(serial_queue_handle_t *queue_handle) +static inline uint32_t serial_queue_length_consumer(serial_queue_handle_t *queue_handle) { - return queue_handle->queue->tail - queue_handle->queue->head; + /* The load-acquire will be paired with the store-release + * in serial_enqueue() or serial_update_shared_tail(). + */ + uint32_t tail = load_acquire_32(&queue_handle->queue->tail); + uint32_t head = queue_handle->queue->head; + return tail - head; } /** - * Check if the queue is empty. + * Return the number of bytes of data stored in the queue. This is calculated by + * using the head and tail values currently stored in the shared queue handle + * data structure. This function should only be called by the PRODUCER of the + * queue. + * + * @param queue_handle queue containing the data. + * + * @return The number bytes of data stored in the queue. + */ +static inline uint32_t serial_queue_length_producer(serial_queue_handle_t *queue_handle) +{ + uint32_t tail = queue_handle->queue->tail; + /* The load-acquire will be paired with the store-release + * in serial_dequeue() or serial_update_shared_head(). + */ + uint32_t head = load_acquire_32(&queue_handle->queue->head); + return tail - head; +} + +/** + * Check if the queue is empty. This function should only be called by the + * CONSUMER of the queue. * * @param queue_handle queue to check. * @param local_head head which points to the next character to be dequeued. + * Should be set to the value of the shared head in the queue if a local copy is + * not in use. * * @return true indicates the queue is empty, false otherwise. */ static inline int serial_queue_empty(serial_queue_handle_t *queue_handle, uint32_t local_head) { - return local_head == queue_handle->queue->tail; + /* The load-acquire will be paired with the store-release + * in serial_enqueue() or serial_update_shared_tail(). + */ + uint32_t tail = load_acquire_32(&queue_handle->queue->tail); + + return local_head == tail; } /** - * Check if the queue is full. + * Check if the queue is full. This function should only be called by the + * PRODUCER of the queue. * * @param queue_handle queue to check. - * @param local_tail tail which points to the next enqueue slot. + * @param local_tail tail which points to the next enqueue slot. Should be set + * to the value of the shared tail in the queue if a local copy is not in use. * * @return true indicates the queue is full, false otherwise. */ static inline int serial_queue_full(serial_queue_handle_t *queue_handle, uint32_t local_tail) { - return local_tail - queue_handle->queue->head == queue_handle->capacity; + /* The load-acquire will be paired with the store-release + * in serial_dequeue() or serial_update_shared_head(). + */ + uint32_t head = load_acquire_32(&queue_handle->queue->head); + + return local_tail - head == queue_handle->capacity; } /** - * Enqueue a character into a queue. Update the shared tail so the character - * is visible to the consumer. + * Enqueue a character into a queue. Update the shared tail so the character is + * visible to the consumer. This function should only be called by the PRODUCER + * of the queue. * * @param queue_handle queue to enqueue into. * @param character character to be enqueued. @@ -84,14 +137,17 @@ static inline int serial_enqueue(serial_queue_handle_t *queue_handle, char chara } queue_handle->data_region[*tail % queue_handle->capacity] = character; - (*tail)++; + + /* The store-release will synchronise with load-acquires by the CONSUMER of the queue. */ + store_release_32(tail, *tail + 1); return 0; } /** * Enqueue a character locally into a queue. Update a local tail variable so the - * character is not visible to the consumer. + * character is not visible to the consumer. This function should only be called + * by the PRODUCER of the queue. * * @param queue_handle queue to enqueue into. * @param local_tail address of the tail to be used and incremented. @@ -112,8 +168,9 @@ static inline int serial_enqueue_local(serial_queue_handle_t *queue_handle, uint } /** - * Dequeue a character from a queue. Update the shared head so the removal of the - * character is visible to the producer. + * Dequeue a character from a queue. Update the shared head so the removal of + * the character is visible to the producer. This function should only be called + * by the CONSUMER of the queue. * * @param queue_handle queue to dequeue from. * @param character address of character to copy into. @@ -129,14 +186,17 @@ static inline int serial_dequeue(serial_queue_handle_t *queue_handle, char *char } *character = queue_handle->data_region[*head % queue_handle->capacity]; - (*head)++; + + /* The store-release will synchronise with load-acquires by the PRODUCER of the queue. */ + store_release_32(head, *head + 1); return 0; } /** * Dequeue a character locally from a queue. Update a local head variable so the - * removal of the character is not visible to the producer. + * removal of the character is not visible to the producer. This function should + * only be called by the CONSUMER of the queue. * * @param queue_handle queue to dequeue from. * @param local_head address of the head to be used and incremented. @@ -157,55 +217,69 @@ static inline int serial_dequeue_local(serial_queue_handle_t *queue_handle, uint } /** - * Update the value of the tail in the shared data structure to make - * locally enqueued data visible. + * Update the value of the tail in the shared data structure to make locally + * enqueued data visible. This function should only be called by the PRODUCER of + * the queue. * * @param queue_handle queue to update. * @param local_tail tail which points to the last character enqueued. */ static inline void serial_update_shared_tail(serial_queue_handle_t *queue_handle, uint32_t local_tail) { - uint32_t current_length = serial_queue_length(queue_handle); - uint32_t new_length = local_tail - queue_handle->queue->head; +#ifdef CONFIG_DEBUG_BUILD + /* The load-acquire will be paired with the store-release + * in serial_dequeue() or serial_update_shared_head(). + */ + uint32_t head = load_acquire_32(&queue_handle->queue->head); + uint32_t current_tail = queue_handle->queue->tail; + + uint32_t current_length = current_tail - head; + uint32_t new_length = local_tail - head; - /* Ensure updates to tail don't overwrite existing data */ + /* Ensure updates to tail do not decrease data length */ assert(new_length >= current_length); /* Ensure updates to tail don't exceed capacity restraints */ assert(new_length <= queue_handle->capacity); - -#ifdef CONFIG_ENABLE_SMP_SUPPORT - THREAD_MEMORY_RELEASE(); #endif - queue_handle->queue->tail = local_tail; + /* The store-release will synchronise with load-acquires by the CONSUMER of the queue. */ + store_release_32(&queue_handle->queue->tail, local_tail); } /** - * Update the value of the head in the shared data structure to make - * local dequeues visible. + * Update the value of the head in the shared data structure to make local + * dequeues visible. This function should only be called by the CONSUMER of the + * queue. * * @param queue_handle queue to update. * @param local_head head which points to the next character to dequeue. */ static inline void serial_update_shared_head(serial_queue_handle_t *queue_handle, uint32_t local_head) { - uint32_t current_length = serial_queue_length(queue_handle); - uint32_t new_length = queue_handle->queue->tail - local_head; - - /* Ensure updates to head don't corrupt queue or capacity constraints */ +#ifdef CONFIG_DEBUG_BUILD + /* The load-acquire will be paired with the store-release + * in serial_enqueue() or serial_update_shared_tail(). + */ + uint32_t tail = load_acquire_32(&queue_handle->queue->tail); + uint32_t current_head = queue_handle->queue->head; + + uint32_t current_length = tail - current_head; + uint32_t new_length = tail - local_head; + + /* Ensure updates to head don't increase data length or violate capacity + constraints */ assert(new_length <= current_length); - -#ifdef CONFIG_ENABLE_SMP_SUPPORT - THREAD_MEMORY_RELEASE(); #endif - queue_handle->queue->head = local_head; + /* The store-release will synchronise with load-acquires by the PRODUCER of the queue. */ + store_release_32(&queue_handle->queue->head, local_head); } /** - * Return the number of bytes of data stored contiguously in the queue from - * the head index to either the tail index or the end of the data region. + * Return the number of bytes of data stored contiguously in the queue from the + * head index to either the tail index or the end of the data region. This + * function should only be called by the CONSUMER of the queue. * * @param queue_handle queue containing the data. * @@ -213,13 +287,16 @@ static inline void serial_update_shared_head(serial_queue_handle_t *queue_handle */ static inline uint32_t serial_queue_contiguous_length(serial_queue_handle_t *queue_handle) { - return MIN(queue_handle->capacity - (queue_handle->queue->head % queue_handle->capacity), - serial_queue_length(queue_handle)); + uint32_t head = queue_handle->queue->head; + uint32_t length = serial_queue_length_consumer(queue_handle); + + return MIN(queue_handle->capacity - (head % queue_handle->capacity), length); } /** * Return the number of free bytes remaining in the queue. This is the number of - * bytes that can be enqueued until the queue is full. + * bytes that can be enqueued until the queue is full. This function should only + * be called by the PRODUCER of the queue. * * @param queue_handle queue to be filled with data. * @@ -227,12 +304,16 @@ static inline uint32_t serial_queue_contiguous_length(serial_queue_handle_t *que */ static inline uint32_t serial_queue_free(serial_queue_handle_t *queue_handle) { - return queue_handle->capacity - serial_queue_length(queue_handle); + uint32_t length = serial_queue_length_producer(queue_handle); + + return queue_handle->capacity - length; } /** - * Return the number of bytes that can be copied into the queue contiguously. This - * is the number of bytes that can be copied into the queue with a single call of memcpy. + * Return the number of bytes that can be copied into the queue contiguously. + * This is the number of bytes that can be copied into the queue with a single + * call of memcpy. This function should only be called by the PRODUCER of the + * queue. * * @param queue_handle queue to be filled with data. * @@ -245,7 +326,8 @@ static inline uint32_t serial_queue_contiguous_free(serial_queue_handle_t *queue } /** - * Enqueue a buffer of contiguous characters into a queue. + * Enqueue a buffer of contiguous characters into a queue. This function should + * only be called by the PRODUCER of the queue. * * @param queue_handle queue to be filled with data. * @param num number of characters to enqueue. @@ -276,9 +358,10 @@ static inline uint32_t serial_enqueue_batch(serial_queue_handle_t *queue_handle, } /** - * Transfer all data from a consumer queue to a producer queue. Assumes there - * is enough free space in the free queue to fit all data in the active - * queue. + * Transfer all data from a consumer queue to a producer queue. Assumes there is + * enough free space in the free queue to fit all data in the active queue. This + * function should only be called by the CONSUMER of the active queue, and the + * PRODUCER of the free queue. * * @param free_queue_handle queue to produce into. * @param active_queue_handle queue to consume. @@ -286,25 +369,43 @@ static inline uint32_t serial_enqueue_batch(serial_queue_handle_t *queue_handle, static inline void serial_transfer_all(serial_queue_handle_t *free_queue_handle, serial_queue_handle_t *active_queue_handle) { - assert(serial_queue_length(active_queue_handle) <= serial_queue_free(free_queue_handle)); + /* The caller is the consumer of the active queue */ + uint32_t active_capacity = active_queue_handle->capacity; + uint32_t active_head = active_queue_handle->queue->head; + uint32_t active_length = load_acquire_32(&active_queue_handle->queue->tail) - active_head; + +#ifdef CONFIG_DEBUG_BUILD + /* The caller is the producer of the free queue. + * The load-acquire will be paired with the store-release + * in serial_dequeue() or serial_update_shared_head() + */ + uint32_t free_length = serial_queue_free(free_queue_handle); + + assert(active_length <= free_length); +#endif /* Copy in contiguous chunks */ - while (serial_queue_length(active_queue_handle)) { - uint32_t num_active = serial_queue_contiguous_length(active_queue_handle); - char *src = active_queue_handle->data_region - + (active_queue_handle->queue->head % active_queue_handle->capacity); - - uint32_t transferred = serial_enqueue_batch(free_queue_handle, num_active, src); - assert(transferred == num_active); - - serial_update_shared_head(active_queue_handle, active_queue_handle->queue->head + num_active); + while (active_length) { + uint32_t active_batch = MIN(active_capacity - (active_head % active_capacity), active_length); + char *src = active_queue_handle->data_region + (active_head % active_capacity); + + uint32_t transferred = serial_enqueue_batch(free_queue_handle, active_batch, src); + assert(transferred == active_batch); + + active_head += active_batch; + serial_update_shared_head(active_queue_handle, active_head); + /* The load-acquire will be paired with the store-release + * in serial_enqueue() or serial_update_shared_tail(). + */ + active_length = load_acquire_32(&active_queue_handle->queue->tail) - active_head; } } /** * Transfer all data from a consumer queue to a producer queue, adding colour codes * before and after. Assumes there is enough free space in the free queue to fit - * all data in the active. + * all data in the active. This function should only be called by the CONSUMER + * of the active queue, and the PRODUCER of the free queue. * * @param free_queue_handle queue to produce into. * @param active_queue_handle queue to consume. @@ -317,8 +418,15 @@ static inline void serial_transfer_all_colour(serial_queue_handle_t *free_queue_ serial_queue_handle_t *active_queue_handle, const char *col_start, uint16_t col_start_len, const char *col_end, uint16_t col_end_len) { - assert(serial_queue_length(active_queue_handle) + col_start_len + col_end_len - <= serial_queue_free(free_queue_handle)); +#ifdef CONFIG_DEBUG_BUILD + /* The caller is the consumer of the active queue */ + uint32_t active_length = serial_queue_length_consumer(active_queue_handle); + + /* The caller is the producer of the free queue */ + uint32_t free_length = serial_queue_free(free_queue_handle); + + assert(active_length + col_start_len + col_end_len <= free_length); +#endif /* Transfer col_start string */ uint32_t transferred = serial_enqueue_batch(free_queue_handle, col_start_len, col_start); diff --git a/include/sddf/util/fence.h b/include/sddf/util/fence.h index 2baaaab4a..594b78d17 100644 --- a/include/sddf/util/fence.h +++ b/include/sddf/util/fence.h @@ -6,6 +6,8 @@ #pragma once +#include + /* Prevent the compiler from re-ordering any read or write across the fence. */ #define COMPILER_MEMORY_FENCE() __atomic_signal_fence(__ATOMIC_ACQ_REL) @@ -34,3 +36,63 @@ * forcing all loads beyond this point to occur after this point. */ #define THREAD_MEMORY_ACQUIRE() __atomic_thread_fence(__ATOMIC_ACQUIRE) + +/* load_acquire_32: synchronises with a store_release_32 that writes the same value to the same location + */ +static inline uint32_t load_acquire_32(const uint32_t *ptr) +{ +#ifdef CONFIG_ENABLE_SMP_SUPPORT + return __atomic_load_n(ptr, __ATOMIC_ACQUIRE); +#else + uint32_t ret = __atomic_load_n(ptr, __ATOMIC_RELAXED); + __atomic_signal_fence(__ATOMIC_ACQUIRE); + return ret; +#endif +} + +/* store_release_32: synchronises with a load_acquire_32 to the same location + */ +static inline void store_release_32(uint32_t *ptr, uint32_t value) +{ +#ifdef CONFIG_ENABLE_SMP_SUPPORT + __atomic_store_n(ptr, value, __ATOMIC_RELEASE); +#else + __atomic_signal_fence(__ATOMIC_RELEASE); + __atomic_store_n(ptr, value, __ATOMIC_RELAXED); +#endif +} + +static inline uint32_t load_relaxed_32(const uint32_t *ptr) +{ + return __atomic_load_n(ptr, __ATOMIC_RELAXED); +} + +/* load_acquire_16: synchronises with a store_release_16 that writes the same value to the same location + */ +static inline uint16_t load_acquire_16(const uint16_t *ptr) +{ +#ifdef CONFIG_ENABLE_SMP_SUPPORT + return __atomic_load_n(ptr, __ATOMIC_ACQUIRE); +#else + uint16_t ret = __atomic_load_n(ptr, __ATOMIC_RELAXED); + __atomic_signal_fence(__ATOMIC_ACQUIRE); + return ret; +#endif +} + +/* store_release_16: synchronises with a load_acquire_16 to the same location + */ +static inline void store_release_16(uint16_t *ptr, uint16_t value) +{ +#ifdef CONFIG_ENABLE_SMP_SUPPORT + __atomic_store_n(ptr, value, __ATOMIC_RELEASE); +#else + __atomic_signal_fence(__ATOMIC_RELEASE); + __atomic_store_n(ptr, value, __ATOMIC_RELAXED); +#endif +} + +static inline uint16_t load_relaxed_16(const uint16_t *ptr) +{ + return __atomic_load_n(ptr, __ATOMIC_RELAXED); +} diff --git a/serial/components/virt_tx.c b/serial/components/virt_tx.c index d7cc4e651..9fd5005a4 100644 --- a/serial/components/virt_tx.c +++ b/serial/components/virt_tx.c @@ -83,7 +83,7 @@ bool process_tx_queue(uint32_t client) return false; } - uint32_t length = serial_queue_length(handle); + uint32_t length = serial_queue_length_consumer(handle); if (config.enable_colour) { const char *client_colour = colours[client % ARRAY_SIZE(colours)]; assert(COLOUR_BEGIN_LEN == strlen(client_colour));