Spinroot

mausys

Member

Registered: 2025-05-03

Posts: 1

verification of my algorithm

I’ve implemented a wait-free, zero-copy circular message queue algorithm designed for a single producer and a single consumer. When the queue is full, the producer discards the oldest message to add a new message. You can find the algorithm here:
https://github.com/mausys/message-queue/blob/main/msgq.c
This queue will be the core of my real-time inter-process communication library, so correctness and reliability are critical. I’m currently looking for ways to formally verify its correctness.
Spin/Modex seems like exactly the right tools for this, thank you for making such excellent tools available.
I’ve adapted the algorithm to Modex-compatible C:
https://github.com/mausys/message-queue/blob/main/spin/mx_msgq.c
Running it with "modex -run mx_msgq.c" shows no errors.
The test checks only a single condition: the producer and consumer must never access the same message at the same time.
Is this test sufficient for verifying the correctness of the algorithm?
Is my assumption correct that Modex does not account for potential memory access reordering by the compiler or the CPU?

spinroot

forum

Registered: 2010-11-18

Posts: 702

Website

Re: verification of my algorithm

that is true -- to account of out of order memory access you'd need to extend the model
an example of what it takes to do this is:
https://spinroot.com/spin/Doc/course/x86_tso.pml