Argentina had 5 in 11 days 🤪

We presented a generalization of recurrence sets to concurrent programs having execution-based semantics.

Despite the name, this works not only for weak memory models, but also for unfair schedulers (aka weak progress guarantees).

Preprint coming soon. Stay tuned!

"I just got my first POPL paper!"

Happy to share that "Recurrence Sets for Proving Fair Non-termination under Axiomatic Memory Consistency Model" has been **conditionally** accepted to appear at POPL 2026.

On his blog post, @hillelwayne.com challenges the correctness of scientific code. He is 100%, from my experience of finding bugs in my own experiments late in the process. A few suggestions to minimize this issue: wiki.alcidesfonseca.com/blog/trust-i...

SIGARCH The ACM Special Interest Group on Computer Architecture

GPU Memory Consistency: Specifications, Testing, and Opportunities for Performance Tooling

www.sigarch.org/blog/

The talk ended with "promises" about future work on how CXL interacts with weak memory. Looking forward to that 😍

On my way to ASPLOS / Eurosys ... Who from my network is also attending?

Despite our efforts over the years to make the tool scalable and practical, I am still surprised to see that while our focus is on weak memory models, we are still competitive against SOTA tools specialized for Sequential Consistency.

The results of the 14th Competition on Software Verification (SV-COMP 2025) are out.

Dartagnan (github.com/hernanponced...) got silver in the verification track (sv-comp.sosy-lab.org/2025/results...) and gold in the validation track (sv-comp.sosy-lab.org/2025/results...) of concurrent programs!

GitHub - open-s4c/libvsync: A verified library of synchronization primitives and concurrent data structures A verified library of synchronization primitives and concurrent data structures - GitHub - open-s4c/libvsync: A verified library of synchronization primitives and concurrent data structures

This project is a key component in libvsync (github.com/open-s4c/lib...), a verified library of synchronization primitives and concurrent data structures.

GitHub - hernanponcedeleon/Dat3M: A verification tool for many memory models A verification tool for many memory models. Contribute to hernanponcedeleon/Dat3M development by creating an account on GitHub.

The memory ordering guarantees provided by the atomic interface are formally described in the VSync Memory Model. Users can use it to verify the correctness of their algorithms with a model checker such as dartagnan (github.com/hernanponced...) or vsyncer (github.com/open-s4c/vsy...).

We are happy to announce the release of the standalone vatomic library (github.com/open-s4c/vat...). This is a header library of atomics operations, supporting mainstream architectures: ARMv7, ARMv8 (AArch32 and AArch64), RISC-V, and x86_64.

One of my regrets from my time as a master student is that I never attended RIO.

Enjoy!

FOSDEM 2025 - Multicore & Concurrency: Algorithms, Performance, Correctness

Are you attending #FOSDEM next weekend in Brussels? Join us for the BOG track "Multicore & Concurrency: Algorithms, Performance, Correctness"

fosdem.org/2025/schedul...

I remember a situation we faced where some verified code using futexes ended up hanging on the real system. The problem was that the abstraction we chose for the futex was sound for safety, but unsound for liveness. A solution for the later resulted in the verification being 10x slower

👍 ... DM

Only in the states?