Introduce c/libvsync concurrency benchmarks

Diogo Behrensrequested to merge
db711/sv-benchmarks:add-c-libvsync into main

This directory contains real-world concurrency-related benchmarks based on a subset of libvsync, a verified library of synchronization primitives and concurrent data structures. With these benchmarks we hope to reduce the gap between academic tools and industry needs.

Note that the orignal code has been verified and optimized for weak memory models. In this directory, however, two modifications have been made:

  • all atomic accesses are upgraded to be sequentially consistent,
  • some algorithms have injected bugs that cause safety violations.

The files in this directory are organized as follows:

  • src/include/: libvsync v4.0.1 (without injected bugs)
  • src/test/: selected test cases
  • src/bugs.patch: patch of injected bugs
  • *.i: expanded test cases with C compiler GNU 9.4.0
  • *.yml: SV-COMP configuration files

Note: the files in src are only for reference, they do not affect the pre-expanded test cases

The full library without injected bugs is available here:

https://github.com/open-s4c/libvsync

Reference:

VSync: push-button verification and optimization for synchronization primitives on weak memory models - Jonas Oberhauser, Rafael Lourenco de Lima Chehab, Diogo Behrens, Ming Fu, Antonio Paolillo, Lilith Oberhauser, Koustubha Bhat, Yuzhong Wen, Haibo Chen, Jaeho Kim, Viktor Vafeiadis - ASPLOS 2021.

Check list:

  • programs added to new and appropriately named directory
  • license present and acceptable (in machine-readable comment at beginning of program as specified by the REUSE project)
  • contributed-by present (either in README file or as comment at beginning of program)
  • programs added to a .set file of an existing category, or new sub-category established (if justified)
  • suggest to add it to benchmark definitions (.XML) in repositories for benchmark-definitions
  • intended property matches the corresponding .prp file
  • programs and expected answer added to a .yml file according to task definitions
  • data model present in task-definition file
  • original (ideally not preprocessed) sources present
  • preprocessed files present
  • preprocessed files generated with correct architecture
  • Makefile added with correct content and without overly broad suppression of warnings

Signed-off-by: Diogo Behrens diogo.behrens@huawei.com

Edited by Diogo Behrens

Merge request reports