Bug#1124402: ITP: herdtools7 -- A tool suite to test weak memory models
Package: wnpp
X-Debbugs-Cc: debian-devel@lists.debian.org
Owner: Sebastian Andrzej Siewior <sebastian@breakpoint.cc>
X-Debbugs-Cc: sebastian@breakpoint.cc
X-Debbugs-Cc: debian-ocaml-maint@lists.debian.org
Severity: wishlist
* Package name : herdtools7
Version : 7.58
Upstream Contact: diy-devel@inria.fr
* URL : https://github.com/herd/herdtools7
* License : CeCILL-B
Programming Lang: ocaml
Description : A tool suite to test weak memory models.
>From upstream description:
| We provide the following tools:
| - herd7: a generic simulator for weak memory models
| - litmus7: run litmus tests (given as assembler programs for Power, ARM, AArch64
| or X86) to test the memory model of the executing machine
| - diy7: produce litmus tests from concise specifications
| some additional tools In particular,
| - mcompare7 to analyse run logs of both herd and litmus.
| - klitmus7, an experimental tool, similar to litmus7 that runs kernel
| memory model tests as kernel modules. The tool klitmus7 is inspired
| from a python script by Andrea Parri.
|
| herdtools7 is the successor of the diy tool suite.
herd7 from this toolsuite is used to verify code based on the Linux
Kernel Memory Model.
The tool is writtin in ocaml. It would be nice if it coul stay under
within the ocaml team. I prepared an initial package at
https://salsa.debian.org/bigeasy/herdtools7
but my ocaml is very weak.
Sebastian
Reply to: