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!

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

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.

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

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...).

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

Enjoy!

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?