NOTICE: This package has been removed from pkgsrc

./wip/vatomic, Formally verified atomic operations

[ CVSweb ] [ Homepage ] [ RSS ] [ Required by ]

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

# VSync atomics - formally-verified atomic operations library

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)