./devel/vatomic, Formally verified atomic operations

[ CVSweb ] [ Homepage ] [ RSS ] [ Required by ] [ Add to tracker ]

Branch: CURRENT, Version: 2.3.1, Package name: vatomic-2.3.1, Maintainer: db7

vatomic is a header library of *atomics operations*, supporting
mainstream architectures: ARMv7, ARMv8 (AArch32 and AArch64),
RISC-V, and x86_64. The memory ordering guarantees provided by the
atomic interface are formally described in the VSync Memory Model
(VMM) file (vmm.cat).

Users can use the vmm.cat file to verify the correctness of their
algorithms with a model checker that supports .cat files.

The atomics implementations are being gradually verified to comply
with VMM. At the moment, we have completed the verification of
ARMv8 64-bits with and without LSE instructions.

Master sites:

Filesize: 171.2 KB

Version history: (Expand)

CVS history: (Expand)


   2025-03-30 09:57:10 by Thomas Klausner | Files touched by this commit (5) 
Log message:
devel/vatomic: Add vatomic version 2.3.1

A formally verified, header-only library of atomics operations supporting ARMv7,
ARMv8 (AArch32 and AArch64), RISC-V, and x86_64.

Packaged in wip by db7