<?xml version="1.0" encoding="utf-8"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" lang="en" xml:lang="en">
<head>
<!-- 2022-02-22 Tue 22:32 -->
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<meta name="viewport" content="width=device-width, initial-scale=1" />
<title><font style="font-variant: small-caps">GenMC</font>: A Generic Model Checker for C Programs</title>
<meta name="generator" content="Org mode" />
<style type="text/css">
 <!--/*--><![CDATA[/*><!--*/
  .title  { text-align: center;
             margin-bottom: .2em; }
  .subtitle { text-align: center;
              font-size: medium;
              font-weight: bold;
              margin-top:0; }
  .todo   { font-family: monospace; color: red; }
  .done   { font-family: monospace; color: green; }
  .priority { font-family: monospace; color: orange; }
  .tag    { background-color: #eee; font-family: monospace;
            padding: 2px; font-size: 80%; font-weight: normal; }
  .timestamp { color: #bebebe; }
  .timestamp-kwd { color: #5f9ea0; }
  .org-right  { margin-left: auto; margin-right: 0px;  text-align: right; }
  .org-left   { margin-left: 0px;  margin-right: auto; text-align: left; }
  .org-center { margin-left: auto; margin-right: auto; text-align: center; }
  .underline { text-decoration: underline; }
  #postamble p, #preamble p { font-size: 90%; margin: .2em; }
  p.verse { margin-left: 3%; }
  pre {
    border: 1px solid #ccc;
    box-shadow: 3px 3px 3px #eee;
    padding: 8pt;
    font-family: monospace;
    overflow: auto;
    margin: 1.2em;
  }
  pre.src {
    position: relative;
    overflow: visible;
    padding-top: 1.2em;
  }
  pre.src:before {
    display: none;
    position: absolute;
    background-color: white;
    top: -10px;
    right: 10px;
    padding: 3px;
    border: 1px solid black;
  }
  pre.src:hover:before { display: inline;}
  /* Languages per Org manual */
  pre.src-asymptote:before { content: 'Asymptote'; }
  pre.src-awk:before { content: 'Awk'; }
  pre.src-C:before { content: 'C'; }
  /* pre.src-C++ doesn't work in CSS */
  pre.src-clojure:before { content: 'Clojure'; }
  pre.src-css:before { content: 'CSS'; }
  pre.src-D:before { content: 'D'; }
  pre.src-ditaa:before { content: 'ditaa'; }
  pre.src-dot:before { content: 'Graphviz'; }
  pre.src-calc:before { content: 'Emacs Calc'; }
  pre.src-emacs-lisp:before { content: 'Emacs Lisp'; }
  pre.src-fortran:before { content: 'Fortran'; }
  pre.src-gnuplot:before { content: 'gnuplot'; }
  pre.src-haskell:before { content: 'Haskell'; }
  pre.src-hledger:before { content: 'hledger'; }
  pre.src-java:before { content: 'Java'; }
  pre.src-js:before { content: 'Javascript'; }
  pre.src-latex:before { content: 'LaTeX'; }
  pre.src-ledger:before { content: 'Ledger'; }
  pre.src-lisp:before { content: 'Lisp'; }
  pre.src-lilypond:before { content: 'Lilypond'; }
  pre.src-lua:before { content: 'Lua'; }
  pre.src-matlab:before { content: 'MATLAB'; }
  pre.src-mscgen:before { content: 'Mscgen'; }
  pre.src-ocaml:before { content: 'Objective Caml'; }
  pre.src-octave:before { content: 'Octave'; }
  pre.src-org:before { content: 'Org mode'; }
  pre.src-oz:before { content: 'OZ'; }
  pre.src-plantuml:before { content: 'Plantuml'; }
  pre.src-processing:before { content: 'Processing.js'; }
  pre.src-python:before { content: 'Python'; }
  pre.src-R:before { content: 'R'; }
  pre.src-ruby:before { content: 'Ruby'; }
  pre.src-sass:before { content: 'Sass'; }
  pre.src-scheme:before { content: 'Scheme'; }
  pre.src-screen:before { content: 'Gnu Screen'; }
  pre.src-sed:before { content: 'Sed'; }
  pre.src-sh:before { content: 'shell'; }
  pre.src-sql:before { content: 'SQL'; }
  pre.src-sqlite:before { content: 'SQLite'; }
  /* additional languages in org.el's org-babel-load-languages alist */
  pre.src-forth:before { content: 'Forth'; }
  pre.src-io:before { content: 'IO'; }
  pre.src-J:before { content: 'J'; }
  pre.src-makefile:before { content: 'Makefile'; }
  pre.src-maxima:before { content: 'Maxima'; }
  pre.src-perl:before { content: 'Perl'; }
  pre.src-picolisp:before { content: 'Pico Lisp'; }
  pre.src-scala:before { content: 'Scala'; }
  pre.src-shell:before { content: 'Shell Script'; }
  pre.src-ebnf2ps:before { content: 'ebfn2ps'; }
  /* additional language identifiers per "defun org-babel-execute"
       in ob-*.el */
  pre.src-cpp:before  { content: 'C++'; }
  pre.src-abc:before  { content: 'ABC'; }
  pre.src-coq:before  { content: 'Coq'; }
  pre.src-groovy:before  { content: 'Groovy'; }
  /* additional language identifiers from org-babel-shell-names in
     ob-shell.el: ob-shell is the only babel language using a lambda to put
     the execution function name together. */
  pre.src-bash:before  { content: 'bash'; }
  pre.src-csh:before  { content: 'csh'; }
  pre.src-ash:before  { content: 'ash'; }
  pre.src-dash:before  { content: 'dash'; }
  pre.src-ksh:before  { content: 'ksh'; }
  pre.src-mksh:before  { content: 'mksh'; }
  pre.src-posh:before  { content: 'posh'; }
  /* Additional Emacs modes also supported by the LaTeX listings package */
  pre.src-ada:before { content: 'Ada'; }
  pre.src-asm:before { content: 'Assembler'; }
  pre.src-caml:before { content: 'Caml'; }
  pre.src-delphi:before { content: 'Delphi'; }
  pre.src-html:before { content: 'HTML'; }
  pre.src-idl:before { content: 'IDL'; }
  pre.src-mercury:before { content: 'Mercury'; }
  pre.src-metapost:before { content: 'MetaPost'; }
  pre.src-modula-2:before { content: 'Modula-2'; }
  pre.src-pascal:before { content: 'Pascal'; }
  pre.src-ps:before { content: 'PostScript'; }
  pre.src-prolog:before { content: 'Prolog'; }
  pre.src-simula:before { content: 'Simula'; }
  pre.src-tcl:before { content: 'tcl'; }
  pre.src-tex:before { content: 'TeX'; }
  pre.src-plain-tex:before { content: 'Plain TeX'; }
  pre.src-verilog:before { content: 'Verilog'; }
  pre.src-vhdl:before { content: 'VHDL'; }
  pre.src-xml:before { content: 'XML'; }
  pre.src-nxml:before { content: 'XML'; }
  /* add a generic configuration mode; LaTeX export needs an additional
     (add-to-list 'org-latex-listings-langs '(conf " ")) in .emacs */
  pre.src-conf:before { content: 'Configuration File'; }

  table { border-collapse:collapse; }
  caption.t-above { caption-side: top; }
  caption.t-bottom { caption-side: bottom; }
  td, th { vertical-align:top;  }
  th.org-right  { text-align: center;  }
  th.org-left   { text-align: center;   }
  th.org-center { text-align: center; }
  td.org-right  { text-align: right;  }
  td.org-left   { text-align: left;   }
  td.org-center { text-align: center; }
  dt { font-weight: bold; }
  .footpara { display: inline; }
  .footdef  { margin-bottom: 1em; }
  .figure { padding: 1em; }
  .figure p { text-align: center; }
  .equation-container {
    display: table;
    text-align: center;
    width: 100%;
  }
  .equation {
    vertical-align: middle;
  }
  .equation-label {
    display: table-cell;
    text-align: right;
    vertical-align: middle;
  }
  .inlinetask {
    padding: 10px;
    border: 2px solid gray;
    margin: 10px;
    background: #ffffcc;
  }
  #org-div-home-and-up
   { text-align: right; font-size: 70%; white-space: nowrap; }
  textarea { overflow-x: auto; }
  .linenr { font-size: smaller }
  .code-highlighted { background-color: #ffff00; }
  .org-info-js_info-navigation { border-style: none; }
  #org-info-js_console-label
    { font-size: 10px; font-weight: bold; white-space: nowrap; }
  .org-info-js_search-highlight
    { background-color: #ffff00; color: #000000; font-weight: bold; }
  .org-svg { width: 90%; }
  /*]]>*/-->
</style>
<script type="text/javascript">
/*
@licstart  The following is the entire license notice for the
JavaScript code in this tag.

Copyright (C) 2012-2020 Free Software Foundation, Inc.

The JavaScript code in this tag is free software: you can
redistribute it and/or modify it under the terms of the GNU
General Public License (GNU GPL) as published by the Free Software
Foundation, either version 3 of the License, or (at your option)
any later version.  The code is distributed WITHOUT ANY WARRANTY;
without even the implied warranty of MERCHANTABILITY or FITNESS
FOR A PARTICULAR PURPOSE.  See the GNU GPL for more details.

As additional permission under GNU GPL version 3 section 7, you
may distribute non-source (e.g., minimized or compacted) forms of
that code without the copy of the GNU GPL normally required by
section 4, provided you include this license notice and a URL
through which recipients can access the Corresponding Source.


@licend  The above is the entire license notice
for the JavaScript code in this tag.
*/
<!--/*--><![CDATA[/*><!--*/
 function CodeHighlightOn(elem, id)
 {
   var target = document.getElementById(id);
   if(null != target) {
     elem.cacheClassElem = elem.className;
     elem.cacheClassTarget = target.className;
     target.className = "code-highlighted";
     elem.className   = "code-highlighted";
   }
 }
 function CodeHighlightOff(elem, id)
 {
   var target = document.getElementById(id);
   if(elem.cacheClassElem)
     elem.className = elem.cacheClassElem;
   if(elem.cacheClassTarget)
     target.className = elem.cacheClassTarget;
 }
/*]]>*///-->
</script>
<script type="text/x-mathjax-config">
    MathJax.Hub.Config({
        displayAlign: "center",
        displayIndent: "0em",

        "HTML-CSS": { scale: 100,
                        linebreaks: { automatic: "false" },
                        webFont: "TeX"
                       },
        SVG: {scale: 100,
              linebreaks: { automatic: "false" },
              font: "TeX"},
        NativeMML: {scale: 100},
        TeX: { equationNumbers: {autoNumber: "AMS"},
               MultLineWidth: "85%",
               TagSide: "right",
               TagIndent: ".8em"
             }
});
</script>
<script type="text/javascript"
        src="https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.0/MathJax.js?config=TeX-AMS_HTML"></script>
</head>
<body>
<div id="content">
<h1 class="title"><font style="font-variant: small-caps">GenMC</font>: A Generic Model Checker for C Programs</h1>
<div id="table-of-contents">
<h2>Table of Contents</h2>
<div id="text-table-of-contents">
<ul>
<li><a href="#orgf53056e">1. Introduction </a></li>
<li><a href="#org8556026">2. Basic Usage</a>
<ul>
<li><a href="#org1661258">2.1. A First Example</a></li>
<li><a href="#orgf6be85b">2.2. Reducing the State Space of a Program With <code>assume()</code> Statements </a></li>
<li><a href="#org64ff9aa">2.3. Handling Infinite Loops </a></li>
<li><a href="#orgdd3cce3">2.4. Error Reporting </a></li>
</ul>
</li>
<li><a href="#org504afc8">3. Tool Features </a>
<ul>
<li><a href="#org640f915">3.1. Available Memory Models </a>
<ul>
<li><a href="#orge31017a">3.1.1. Note on LKMM Support</a></li>
<li><a href="#orgd621ff1">3.1.2. Note on Language Memory Models vs Hardware Memory Models</a></li>
</ul>
</li>
<li><a href="#orge6b4202">3.2. Race Detection and Memory Errors</a></li>
<li><a href="#org0aec697">3.3. Lock-Aware Partial Order Reduction (<font style="font-variant: small-caps">LAPOR</font>)</a></li>
<li><a href="#org2d63e5f">3.4. Barrier-Aware Model Checking (<font style="font-variant: small-caps">BAM</font>)</a></li>
<li><a href="#orgcc0984a">3.5. Symmetry Reduction</a></li>
<li><a href="#org38f46c5">3.6. Checking Liveness </a></li>
<li><a href="#org9ed8a7b">3.7. System Calls and Persistency Checks (<font style="font-variant: small-caps">Persevere</font>) </a>
<ul>
<li><a href="#org326b97c">3.7.1. Consistency of File-Manipulating Programs</a></li>
<li><a href="#orgc48d708">3.7.2. Persistency of File-Manipulating Programs</a></li>
</ul>
</li>
</ul>
</li>
<li><a href="#org2085b6d">4. Command-line Options </a></li>
<li><a href="#orgdc94ef2">5. Supported APIs </a>
<ul>
<li><a href="#orgc4fffed">5.1. Supported <code>stdio</code>, <code>unistd</code> and <code>fcntl</code> API</a></li>
<li><a href="#org6f8044c">5.2. Supported <code>stdlib</code> API</a></li>
<li><a href="#org0afb1fd">5.3. Supported <code>pthread</code> API</a></li>
<li><a href="#org211066f">5.4. Supported SV-COMP<sup>6</sup> API</a></li>
</ul>
</li>
<li><a href="#orgb713789">6. Contact </a></li>
<li><a href="#orgb780d83">7. Bibliography </a></li>
</ul>
</div>
</div>


<div id="outline-container-orgf53056e" class="outline-2">
<h2 id="orgf53056e"><span class="section-number-2">1</span> Introduction <a id="org9235871"></a></h2>
<div class="outline-text-2" id="text-1">
<p>
<font style="font-variant: small-caps">GenMC</font> is an effective stateless model checker for programs
written under the RC11,<sup>1</sup> IMM,<sup>2</sup> and LKMM<sup>3</sup> memory models.
<font style="font-variant: small-caps">GenMC</font> verifies safety properties of C programs that use <code>C11</code>
atomics and the <code>pthread</code> library for concurrency. It employs a very
effective dynamic partial order reduction technique
<sup>4,5</sup> that is
sound, complete and optimal.
</p>

<p>
<font style="font-variant: small-caps">GenMC</font> works at the level of LLVM Intermediate Representation (LLVM-IR)
and uses <code>clang</code> to translate C programs to LLVM-IR. This means it
can miss some bugs that are removed during the translation to LLVM-IR,
but it is guaranteed to encounter at least as many bugs as the
compiler backend will encounter.
</p>

<p>
<font style="font-variant: small-caps">GenMC</font> should compile on Linux and Mac OSX provided that the relevant
dependencies are installed.
</p>
</div>
</div>


<div id="outline-container-org8556026" class="outline-2">
<h2 id="org8556026"><span class="section-number-2">2</span> Basic Usage</h2>
<div class="outline-text-2" id="text-2">
<p>
A generic invocation of <font style="font-variant: small-caps">GenMC</font> resembles the following:
</p>

<div class="org-src-container">
<pre class="src src-sh">genmc [OPTIONS] -- [CFLAGS] &lt;file&gt;
</pre>
</div>

<p>
In the above command, <code>OPTIONS</code> include several options that can be
passed to <font style="font-variant: small-caps">GenMC</font> (see Section <a href="#org59fce12">4</a> for more details), and
<code>CFLAGS</code> are the options that one would normally pass to the C
compiler. If no such flags exist, the <code>--</code> can be omitted.
Lastly, <code>file</code> should be a C file that uses the <code>stdatomic.h</code>
and <code>pthread.h</code> APIs for concurrency.
</p>

<p>
Note that, in order for <font style="font-variant: small-caps">GenMC</font> to be able to verify it, <code>file</code>
needs to meet two requirements: finiteness and data-determinism.
Finiteness means that all tests need to have finite traces,
i.e., no infinite loops (these need to be bounded; see
Section <a href="#org7e7ce85">2.3</a>). Data-determinism means that
the code under test should be data-deterministic, i.e.,
not perform actions like calling <code>rand()</code>, performing
actions based on user input or the clock, etc. In other words,
all non-determinism should originate either from the scheduler
or the underlying (weak) memory model.
</p>

<p>
As long as these requirements as satisfied, <font style="font-variant: small-caps">GenMC</font> will detect safety
errors, races on non-atomic variables, as well as some memory errors
(e.g., double-free error). Users can provide safety specifications for
their programs by using <code>assert()</code> statements.
</p>
</div>

<div id="outline-container-org1661258" class="outline-3">
<h3 id="org1661258"><span class="section-number-3">2.1</span> A First Example</h3>
<div class="outline-text-3" id="text-2-1">
<p>
Consider the following program, demonstrating the Message-Passing (MP)
idiom:
</p>

<div class="org-src-container">
<pre class="src src-C"><span style="color: #586e75; font-style: italic;">/* </span><span style="color: #586e75; font-style: italic;">file: mp.c</span><span style="color: #586e75; font-style: italic;"> */</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdlib.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;pthread.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdatomic.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdbool.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;assert.h&gt;</span>

<span style="color: #268bd2;">atomic_int</span> <span style="color: #6c71c4;">data</span>;
<span style="color: #268bd2;">atomic_bool</span> <span style="color: #6c71c4;">ready</span>;

<span style="color: #268bd2;">void</span> *<span style="color: #b58900;">thread_1</span>(<span style="color: #268bd2;">void</span> *<span style="color: #6c71c4;">unused</span>)
{
        atomic_store_explicit(&amp;data, 42, memory_order_relaxed);
        atomic_store_explicit(&amp;ready, <span style="color: #268bd2;">true</span>, memory_order_release);
        <span style="color: #859900;">return</span> <span style="color: #268bd2;">NULL</span>;
}

<span style="color: #268bd2;">void</span> *<span style="color: #b58900;">thread_2</span>(<span style="color: #268bd2;">void</span> *<span style="color: #6c71c4;">unused</span>)
{
        <span style="color: #859900;">if</span> (atomic_load_explicit(&amp;ready, memory_order_acquire)) {
                <span style="color: #268bd2;">int</span> <span style="color: #6c71c4;">d</span> = atomic_load_explicit(&amp;data, memory_order_relaxed);
                assert(d == 42);
        }
        <span style="color: #859900;">return</span> <span style="color: #268bd2;">NULL</span>;
}

<span style="color: #268bd2;">int</span> <span style="color: #b58900;">main</span>()
{
        <span style="color: #268bd2;">pthread_t</span> <span style="color: #6c71c4;">t1</span>, <span style="color: #6c71c4;">t2</span>;

        <span style="color: #859900;">if</span> (pthread_create(&amp;t1, <span style="color: #268bd2;">NULL</span>, thread_1, <span style="color: #268bd2;">NULL</span>))
                abort();
        <span style="color: #859900;">if</span> (pthread_create(&amp;t2, <span style="color: #268bd2;">NULL</span>, thread_2, <span style="color: #268bd2;">NULL</span>))
                abort();

        <span style="color: #859900;">return</span> 0;
}
</pre>
</div>

<p>
In order to analyze the code above with <font style="font-variant: small-caps">GenMC</font>, we can use the
following command:
</p>

<div class="org-src-container">
<pre class="src src-sh">genmc mp.c
</pre>
</div>
<p>
with which <font style="font-variant: small-caps">GenMC</font> will yield the following result:
</p>
<div class="org-src-container">
<pre class="src src-sh">Number of complete executions explored: 2
Total wall-clock time: 0.02s
</pre>
</div>
<p>
<font style="font-variant: small-caps">GenMC</font> explores two executions: one where \(ready = data =0\), and
one where \(ready = data = 1\).
</p>
</div>
</div>


<div id="outline-container-orgf6be85b" class="outline-3">
<h3 id="orgf6be85b"><span class="section-number-3">2.2</span> Reducing the State Space of a Program With <code>assume()</code> Statements <a id="org17d95a6"></a></h3>
<div class="outline-text-3" id="text-2-2">
<p>
In some programs, we only care about what happens when certain reads
read certain values of interest. That said, by default, <font style="font-variant: small-caps">GenMC</font>
will explore all possible values for all program loads, possibly
leading to the exploration of an exponential number of executions.
</p>

<p>
To alleviate this problem, <font style="font-variant: small-caps">GenMC</font> supports the
<code>__VERIFIER_assume()</code> function (similar to the one specified in
SV-COMP<sup>6</sup>). This function takes an integer argument
(e.g., the value read from a load), and only continues the execution
if the argument is non-zero.
</p>

<p>
For example, let us consider the MP program from the previous section,
and suppose that we are only interested in verifying the assertion
in cases where the first read of the second thread reads 1. We can
use an <code>assume()</code> statement to achieve this, as shown below:
</p>

<div class="org-src-container">
<pre class="src src-C"><span style="color: #586e75; font-style: italic;">/* </span><span style="color: #586e75; font-style: italic;">file: mp-assume.c</span><span style="color: #586e75; font-style: italic;"> */</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdlib.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;pthread.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdatomic.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdbool.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;assert.h&gt;</span>

<span style="color: #268bd2;">void</span> <span style="color: #b58900;">__VERIFIER_assume</span>(<span style="color: #268bd2;">int</span>);

<span style="color: #268bd2;">atomic_int</span> <span style="color: #6c71c4;">data</span>;
<span style="color: #268bd2;">atomic_bool</span> <span style="color: #6c71c4;">ready</span>;

<span style="color: #268bd2;">void</span> *<span style="color: #b58900;">thread_1</span>(<span style="color: #268bd2;">void</span> *<span style="color: #6c71c4;">unused</span>)
{
        atomic_store_explicit(&amp;data, 42, memory_order_relaxed);
        atomic_store_explicit(&amp;ready, <span style="color: #268bd2;">true</span>, memory_order_release);
        <span style="color: #859900;">return</span> <span style="color: #268bd2;">NULL</span>;
}

<span style="color: #268bd2;">void</span> *<span style="color: #b58900;">thread_2</span>(<span style="color: #268bd2;">void</span> *<span style="color: #6c71c4;">unused</span>)
{
        <span style="color: #268bd2;">int</span> <span style="color: #6c71c4;">r</span> = atomic_load_explicit(&amp;ready, memory_order_acquire);
        __VERIFIER_assume(r);
        <span style="color: #859900;">if</span> (r) {
                <span style="color: #268bd2;">int</span> <span style="color: #6c71c4;">d</span> = atomic_load_explicit(&amp;data, memory_order_relaxed);
                assert(d == 42);
        }
        <span style="color: #859900;">return</span> <span style="color: #268bd2;">NULL</span>;
}

<span style="color: #268bd2;">int</span> <span style="color: #b58900;">main</span>()
{
        <span style="color: #268bd2;">pthread_t</span> <span style="color: #6c71c4;">t1</span>, <span style="color: #6c71c4;">t2</span>;

        <span style="color: #859900;">if</span> (pthread_create(&amp;t1, <span style="color: #268bd2;">NULL</span>, thread_1, <span style="color: #268bd2;">NULL</span>))
                abort();
        <span style="color: #859900;">if</span> (pthread_create(&amp;t2, <span style="color: #268bd2;">NULL</span>, thread_2, <span style="color: #268bd2;">NULL</span>))
                abort();

        <span style="color: #859900;">return</span> 0;
}
</pre>
</div>
<p>
Note that the <code>__VERIFIER_assume()</code> function has to be declared. Alternatively,
one can include the <code>&lt;genmc.h&gt;</code> header, that contains the declarations for all
the special function that <font style="font-variant: small-caps">GenMC</font> offers (see Section <a href="#org017383e">5</a>).
</p>

<p>
If we run <font style="font-variant: small-caps">GenMC</font> on the <code>mp-assume.c</code> program above, we get the following
output:
</p>
<div class="org-src-container">
<pre class="src src-sh">Number of complete executions explored: 1
Number of blocked executions seen: 1
Total wall-clock time: 0.02s
</pre>
</div>
<p>
As can be seen, <font style="font-variant: small-caps">GenMC</font> only explored one full execution (the one
where \(r = 1\), while the execution where \(r = 0\) was blocked, because
of the <code>assume()</code> statement. Of course, while the usage of <code>assume()</code>
does not make any practical difference in this small example, this is
not always the case: generally, using <code>assume()</code> might yield an
exponential improvement in <font style="font-variant: small-caps">GenMC</font>'s running time.
</p>

<p>
Finally, note that, when using <font style="font-variant: small-caps">GenMC</font> under memory models that
track dependencies (see Section <a href="#org43a1714">3.1</a>), an <code>assume()</code>
statement will introduce a control dependency in the program code.
</p>
</div>
</div>


<div id="outline-container-org64ff9aa" class="outline-3">
<h3 id="org64ff9aa"><span class="section-number-3">2.3</span> Handling Infinite Loops <a id="org7e7ce85"></a></h3>
<div class="outline-text-3" id="text-2-3">
<p>
As mentioned in the beginning of this section, all programs that
<font style="font-variant: small-caps">GenMC</font> can handle need to have finite traces. That said, many
programs of interest do not fulfill this requirement, because, for
example, they have some infinite loop. <font style="font-variant: small-caps">GenMC</font> offers three
solutions for such cases.
</p>

<p>
First, <font style="font-variant: small-caps">GenMC</font> can automatically perform the "spin-assume"
transformation for a large class of spinloops. Specifically, as long
as a spinloop completes a full iteration with no visible side effects
(e.g., stores to global variables), <font style="font-variant: small-caps">GenMC</font> will cut the respective
execution. For instance, consider the following simple loop:
</p>
<div class="org-src-container">
<pre class="src src-C"><span style="color: #268bd2;">int</span> <span style="color: #6c71c4;">r</span> = 0;
<span style="color: #859900;">while</span> (<span style="color: #268bd2;">!</span>atomic_compare_exchange_strong(&amp;x, &amp;r, 1))
        r = 0;
</pre>
</div>
<p>
Since this loop has no visible side-effects whenever it completes
a full iteration, <font style="font-variant: small-caps">GenMC</font> will not explore more than one
execution where the loop fails (the execution where the loop fails
will be reported as a blocked execution). The "spin-assume"
transformation has proven to be very effective for a wide range of
loops; for more details on whether it applies on a specific loop,
please see.<sup>7</sup>
</p>



<p>
Finally, for infinite loops with side effects, we can use the
<code>-unroll=N</code> command-line option (see Section <a href="#org59fce12">4</a>). This option
bounds all loops so that they are executed at most <code>N</code> times.  In this
case, any verification guarantees that <font style="font-variant: small-caps">GenMC</font> provides hold up to
that bound.  If you are unsure whether you should use the <code>-unroll=N</code>
switch, you can try to verify the program and check whether
<font style="font-variant: small-caps">GenMC</font> complains about the graph size
(<code>-warn-on-graph-size=&lt;N&gt;</code>). If it does, there is a good chance you
need to use the <code>-unroll=N</code> switch.
</p>

<p>
Note that the loop-bounding happens at the LLVM-IR level, which means
that the loops there may not directly correspond to loops in the C
code (depending on the enabled compiled optimizations, etc).
</p>
</div>
</div>


<div id="outline-container-orgdd3cce3" class="outline-3">
<h3 id="orgdd3cce3"><span class="section-number-3">2.4</span> Error Reporting <a id="orgfed16b3"></a></h3>
<div class="outline-text-3" id="text-2-4">
<p>
In the previous sections, saw how <font style="font-variant: small-caps">GenMC</font> verifies the small MP program.
Let us now proceed with an erroneous version of this program, in order
to show how <font style="font-variant: small-caps">GenMC</font> reports errors to the user.
</p>

<p>
Consider the following variant of the MP program below, where the
store to <code>ready</code> in the first thread is now performed using a relaxed
access:
</p>
<div class="org-src-container">
<pre class="src src-C"><span style="color: #586e75; font-style: italic;">/* </span><span style="color: #586e75; font-style: italic;">file: mp-error.c</span><span style="color: #586e75; font-style: italic;"> */</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdlib.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;pthread.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdatomic.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdbool.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;assert.h&gt;</span>

<span style="color: #268bd2;">atomic_int</span> <span style="color: #6c71c4;">data</span>;
<span style="color: #268bd2;">atomic_bool</span> <span style="color: #6c71c4;">ready</span>;

<span style="color: #268bd2;">void</span> *<span style="color: #b58900;">thread_1</span>(<span style="color: #268bd2;">void</span> *<span style="color: #6c71c4;">unused</span>)
{
        atomic_store_explicit(&amp;data, 42, memory_order_relaxed);
        atomic_store_explicit(&amp;ready, <span style="color: #268bd2;">true</span>, memory_order_relaxed);
        <span style="color: #859900;">return</span> <span style="color: #268bd2;">NULL</span>;
}

<span style="color: #268bd2;">void</span> *<span style="color: #b58900;">thread_2</span>(<span style="color: #268bd2;">void</span> *<span style="color: #6c71c4;">unused</span>)
{
        <span style="color: #859900;">if</span> (atomic_load_explicit(&amp;ready, memory_order_acquire)) {
                <span style="color: #268bd2;">int</span> <span style="color: #6c71c4;">d</span> = atomic_load_explicit(&amp;data, memory_order_relaxed);
                assert(d == 42);
        }
        <span style="color: #859900;">return</span> <span style="color: #268bd2;">NULL</span>;
}

<span style="color: #268bd2;">int</span> <span style="color: #b58900;">main</span>()
{
        <span style="color: #268bd2;">pthread_t</span> <span style="color: #6c71c4;">t1</span>, <span style="color: #6c71c4;">t2</span>;

        <span style="color: #859900;">if</span> (pthread_create(&amp;t1, <span style="color: #268bd2;">NULL</span>, thread_1, <span style="color: #268bd2;">NULL</span>))
                abort();
        <span style="color: #859900;">if</span> (pthread_create(&amp;t2, <span style="color: #268bd2;">NULL</span>, thread_2, <span style="color: #268bd2;">NULL</span>))
                abort();

        <span style="color: #859900;">return</span> 0;
}
</pre>
</div>
<p>
This program is buggy since the load from <code>ready</code> no longer
synchronizes with the corresponding store, which in turn means that
the load from <code>data</code> may also read 0 (the initial value), and
not just 42.
</p>

<p>
Running <font style="font-variant: small-caps">GenMC</font> on the above program, we get the following outcome:
</p>
<div class="org-src-container">
<pre class="src src-sh">Error detected: Safety violation!
<span style="color: #b58900;">Event</span> (2, 2) <span style="color: #859900;">in</span> graph:
&lt;-1, 0&gt; main:
        (0, 0): B
        (0, 1): M
        (0, 2): M
        (0, 3): TC [forks 1] L.30
        (0, 4): Wna (t1, 1) L.30
        (0, 5): TC [forks 2] L.32
        (0, 6): Wna (t2, 2) L.32
        (0, 7): E
&lt;0, 1&gt; thread_1:
        (1, 0): B
        (1, 1): Wrlx (data, 42) L.12
        (1, 2): Wrlx (ready, 1) L.13
        (1, 3): E
&lt;0, 2&gt; thread_2:
        (2, 0): B
        (2, 1): Racq (ready, 1) [(1, 2)] L.19
        (2, 2): Rrlx (data, 0) [INIT] L.20

Assertion violation: <span style="color: #6c71c4;">d</span> == 42
Number of complete executions explored: 1
Total wall-clock time: 0.02s
</pre>
</div>

<p>
<font style="font-variant: small-caps">GenMC</font> reports an error and prints some information relevant for
debugging. First, it prints the type of the error, then the execution
graph representing the erroneous execution, and finally the error
message, along with the executions explored so far and the time that
was required.
</p>

<p>
The graph contains the events of each thread along with some
information about the corresponding source-code instructions.  For
example, for write events (e.g., event (1, 1)), the access mode, the
name of the variable accessed, the value written, as well as the
corresponding source-code line are printed. The situation is similar
for reads (e.g., event (2, 1)), but also the position in the graph
from which the read is reading from is printed.
</p>

<p>
Note that there are many different types of events. However, many of
them are <font style="font-variant: small-caps">GenMC</font>-related and not of particular interest to users (e.g.,
events labeled with `B', which correspond to the beginning of a
thread). Thus, <font style="font-variant: small-caps">GenMC</font> only prints the source-code lines for events
that correspond to actual user instructions, thus helping the
debugging procedure.
</p>

<p>
Finally, when more information regarding an error are required,
two command-line switches are provided. The <code>-dump-error-graph=&lt;file&gt;</code>
switch provides a visual representation of the erroneous execution,
as it will output the reported graph in DOT format in <code>&lt;file&gt;</code>,
so that it can be viewed by a PDF viewer. Finally, the <code>-print-error-trace</code>
switch will print a sequence of source-code lines leading to
the error. The latter is especially useful for cases where
the bug is not caused by some weak-memory effect but rather from
some particular interleaving (e.g., if all accesses are
 <code>memory_order_seq_cst</code>), and the write where each read is reading
from can be determined simply by locating the previous write in the
same memory location in the sequence.
</p>
</div>
</div>
</div>


<div id="outline-container-org504afc8" class="outline-2">
<h2 id="org504afc8"><span class="section-number-2">3</span> Tool Features <a id="org0648e25"></a></h2>
<div class="outline-text-2" id="text-3">
</div>

<div id="outline-container-org640f915" class="outline-3">
<h3 id="org640f915"><span class="section-number-3">3.1</span> Available Memory Models <a id="org43a1714"></a></h3>
<div class="outline-text-3" id="text-3-1">
<p>
By default, <font style="font-variant: small-caps">GenMC</font> verifies programs under RC11. However, apart
from RC11, <font style="font-variant: small-caps">GenMC</font> also supports IMM and (experimentally) LKMM.
The difference between these memory models (as far as allowed outcomes are concerned)
can be seen in the following program:
</p>

<div class="org-src-container">
<pre class="src src-C"><span style="color: #586e75; font-style: italic;">/* </span><span style="color: #586e75; font-style: italic;">file: lb.c</span><span style="color: #586e75; font-style: italic;"> */</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdlib.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;pthread.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdatomic.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdbool.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;assert.h&gt;</span>

<span style="color: #268bd2;">atomic_int</span> <span style="color: #6c71c4;">x</span>;
<span style="color: #268bd2;">atomic_int</span> <span style="color: #6c71c4;">y</span>;

<span style="color: #268bd2;">void</span> *<span style="color: #b58900;">thread_1</span>(<span style="color: #268bd2;">void</span> *<span style="color: #6c71c4;">unused</span>)
{
        <span style="color: #268bd2;">int</span> <span style="color: #6c71c4;">a</span> = atomic_load_explicit(&amp;x, memory_order_relaxed);
        atomic_store_explicit(&amp;y, 1, memory_order_relaxed);
        <span style="color: #859900;">return</span> <span style="color: #268bd2;">NULL</span>;
}

<span style="color: #268bd2;">void</span> *<span style="color: #b58900;">thread_2</span>(<span style="color: #268bd2;">void</span> *<span style="color: #6c71c4;">unused</span>)
{
        <span style="color: #268bd2;">int</span> <span style="color: #6c71c4;">b</span> = atomic_load_explicit(&amp;y, memory_order_relaxed);
        atomic_store_explicit(&amp;x, 1, memory_order_relaxed);
        <span style="color: #859900;">return</span> <span style="color: #268bd2;">NULL</span>;
}

<span style="color: #268bd2;">int</span> <span style="color: #b58900;">main</span>()
{
        <span style="color: #268bd2;">pthread_t</span> <span style="color: #6c71c4;">t1</span>, <span style="color: #6c71c4;">t2</span>;

        <span style="color: #859900;">if</span> (pthread_create(&amp;t1, <span style="color: #268bd2;">NULL</span>, thread_1, <span style="color: #268bd2;">NULL</span>))
                abort();
        <span style="color: #859900;">if</span> (pthread_create(&amp;t2, <span style="color: #268bd2;">NULL</span>, thread_2, <span style="color: #268bd2;">NULL</span>))
                abort();

        <span style="color: #859900;">return</span> 0;
}
</pre>
</div>

<p>
Under RC11, an execution where both \(a = 1\) and \(b = 1\) is forbidden,
whereas such an execution is allowed under IMM and LKMM. To account for such
behaviors, <font style="font-variant: small-caps">GenMC</font> tracks dependencies between program instructions
thus leading to a constant overhead when verifying programs under
models like IMM.
</p>
</div>

<div id="outline-container-orge31017a" class="outline-4">
<h4 id="orge31017a"><span class="section-number-4">3.1.1</span> Note on LKMM Support</h4>
<div class="outline-text-4" id="text-3-1-1">
<p>
<font style="font-variant: small-caps">GenMC</font>'s support for LKMM is currently at an experimental stage.
<font style="font-variant: small-caps">GenMC</font> includes plain accesses in <span style="color: #808080; font-family: monospace">ppo</span>
(in contrast to what<sup>3</sup> dictates), as plain accesses
to temporary LLVM-IR variables are occasionally generated by <code>clang</code> between
accesses to shared memory, and thus including them in <span style="color: #808080; font-family: monospace">ppo</span> is
necessary to preserve dependencies.
</p>

<p>
Tests that use LKMM atomics need to include <code>&lt;lkmm.h</code>.
</p>
</div>
</div>

<div id="outline-container-orgd621ff1" class="outline-4">
<h4 id="orgd621ff1"><span class="section-number-4">3.1.2</span> Note on Language Memory Models vs Hardware Memory Models</h4>
<div class="outline-text-4" id="text-3-1-2">
<p>
RC11 is a language-level memory model while IMM is a hardware memory
model. Subsequently, the verification results produced by <font style="font-variant: small-caps">GenMC</font>
for the two models should be interpreted somewhat differently.
</p>

<p>
What this means in practice is that, when verifying programs under
RC11, the input file is assumed to be the very source code the user
wrote. A successful verification result under RC11 holds all the
way down to the actual executable, due to the guarantees provided
by RC11.<sup>1</sup>
</p>

<p>
On the other hand, when verifying programs under IMM, the input file
is assumed to be the assembly code run by the processor (or, more
precisely, a program in IMM's intermediate language).  And while
<font style="font-variant: small-caps">GenMC</font> allows the input file to be a C file (as in the case of
RC11), it assumes that this C file corresponds to an assembly file
that is the result of the compilation of some program in IMM's
language. In other words, program correctness is not preserved across
compilation for IMM inputs.
</p>
</div>
</div>
</div>

<div id="outline-container-orge6b4202" class="outline-3">
<h3 id="orge6b4202"><span class="section-number-3">3.2</span> Race Detection and Memory Errors</h3>
<div class="outline-text-3" id="text-3-2">
<p>
For memory models that define the notion of a race, <font style="font-variant: small-caps">GenMC</font> will
report executions containing races erroneous. For instance, under
RC11, the following program is racy, as there is no happens-before
between the write of \(x\) in the first thread and the non-atomic
read of \(x\) in the second thread (even though the latter causally
depends on the former).
</p>

<div class="org-src-container">
<pre class="src src-C"><span style="color: #586e75; font-style: italic;">/* </span><span style="color: #586e75; font-style: italic;">file: race.c</span><span style="color: #586e75; font-style: italic;"> */</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdlib.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;pthread.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdatomic.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdbool.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;assert.h&gt;</span>

<span style="color: #268bd2;">atomic_int</span> <span style="color: #6c71c4;">x</span>;

<span style="color: #268bd2;">void</span> *<span style="color: #b58900;">thread_1</span>(<span style="color: #268bd2;">void</span> *<span style="color: #6c71c4;">unused</span>)
{
        atomic_store_explicit(&amp;x, 1, memory_order_relaxed);
        <span style="color: #859900;">return</span> <span style="color: #268bd2;">NULL</span>;
}

<span style="color: #268bd2;">void</span> *<span style="color: #b58900;">thread_2</span>(<span style="color: #268bd2;">void</span> *<span style="color: #6c71c4;">unused</span>)
{
        <span style="color: #268bd2;">int</span> <span style="color: #6c71c4;">a</span>, <span style="color: #6c71c4;">b</span>;

        a = atomic_load_explicit(&amp;x, memory_order_relaxed);
        <span style="color: #859900;">if</span> (a == 1)
                b = *((<span style="color: #268bd2;">int</span> *) &amp;x);
        <span style="color: #859900;">return</span> <span style="color: #268bd2;">NULL</span>;
}

<span style="color: #268bd2;">int</span> <span style="color: #b58900;">main</span>()
{
        <span style="color: #268bd2;">pthread_t</span> <span style="color: #6c71c4;">t1</span>, <span style="color: #6c71c4;">t2</span>;

        <span style="color: #859900;">if</span> (pthread_create(&amp;t1, <span style="color: #268bd2;">NULL</span>, thread_1, <span style="color: #268bd2;">NULL</span>))
                abort();
        <span style="color: #859900;">if</span> (pthread_create(&amp;t2, <span style="color: #268bd2;">NULL</span>, thread_2, <span style="color: #268bd2;">NULL</span>))
                abort();

        <span style="color: #859900;">return</span> 0;
}
</pre>
</div>

<p>
Additionally, for all memory models, <font style="font-variant: small-caps">GenMC</font> detects some memory
races like accessing memory that has been already freed, accessing
dynamic memory that has not been allocated, or freeing an already
freed chunk of memory.
</p>

<p>
Race detection can be completely disabled by means of
<code>-disable-race-detection</code>, which may yield better performance for
certain programs.
</p>
</div>
</div>

<div id="outline-container-org0aec697" class="outline-3">
<h3 id="org0aec697"><span class="section-number-3">3.3</span> Lock-Aware Partial Order Reduction (<font style="font-variant: small-caps">LAPOR</font>)</h3>
<div class="outline-text-3" id="text-3-3">
<p>
For programs that employ coarse-grained locking schemes <font style="font-variant: small-caps">LAPOR</font>
<sup>8</sup> might greatly reduce the state space
and thus the verification time.  For instance, consider the following
program where a lock is used (overly conservatively) to read a shared
variable:
</p>

<div class="org-src-container">
<pre class="src src-C"><span style="color: #586e75; font-style: italic;">/* </span><span style="color: #586e75; font-style: italic;">file: lapor.c</span><span style="color: #586e75; font-style: italic;"> */</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdlib.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;pthread.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdatomic.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdbool.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;assert.h&gt;</span>

<span style="color: #d33682;">#if</span><span style="color: #d33682;">n</span><span style="color: #d33682;">def</span> N
<span style="color: #d33682;"># define</span> <span style="color: #6c71c4;">N</span> 2
<span style="color: #d33682;">#endif</span>

<span style="color: #268bd2;">pthread_mutex_t</span> <span style="color: #6c71c4;">l</span>;
<span style="color: #268bd2;">int</span> <span style="color: #6c71c4;">x</span>;

<span style="color: #268bd2;">void</span> *<span style="color: #b58900;">thread_n</span>(<span style="color: #268bd2;">void</span> *<span style="color: #6c71c4;">unused</span>)
{
        pthread_mutex_lock(&amp;l);
        <span style="color: #268bd2;">int</span> <span style="color: #6c71c4;">r</span> = x;
        pthread_mutex_unlock(&amp;l);
        <span style="color: #859900;">return</span> <span style="color: #268bd2;">NULL</span>;
}

<span style="color: #268bd2;">int</span> <span style="color: #b58900;">main</span>()
{
        <span style="color: #268bd2;">pthread_t</span> <span style="color: #6c71c4;">t</span>[N];

        <span style="color: #859900;">for</span> (<span style="color: #268bd2;">int</span> <span style="color: #6c71c4;">i</span> = 0; i &lt; N; i++) {
                <span style="color: #859900;">if</span> (pthread_create(&amp;t[i], <span style="color: #268bd2;">NULL</span>, thread_n, <span style="color: #268bd2;">NULL</span>))
                        abort();
        }

        <span style="color: #859900;">return</span> 0;
}
</pre>
</div>

<p>
Running <font style="font-variant: small-caps">GenMC</font> on the program above results in the following outcome:
</p>
<div class="org-src-container">
<pre class="src src-sh">Number of complete executions explored: 2
Total wall-clock time: 0.02s
</pre>
</div>
<p>
As expected, as the value of \(N\) increases, the executions of the
program also increase in an exponential manner.
</p>

<p>
However, if we run <font style="font-variant: small-caps">GenMC</font> with <code>-lapor</code> on the same program, we get the
following output:
</p>
<div class="org-src-container">
<pre class="src src-sh">Number of complete executions explored: 1
Total wall-clock time: 0.02s
</pre>
</div>
<p>
<font style="font-variant: small-caps">LAPOR</font> leverages the fact that the contents of the critical
sections of the threads commute (i.e., the order in which the critical
sections are executed does not matter), and only explores 1 execution
for all values of \(N\).
</p>

<p>
We note that for programs where no further reduction in the
state space is possible, <font style="font-variant: small-caps">LAPOR</font> can be cause a polynomial
slowdown.
</p>
</div>
</div>


<div id="outline-container-org2d63e5f" class="outline-3">
<h3 id="org2d63e5f"><span class="section-number-3">3.4</span> Barrier-Aware Model Checking (<font style="font-variant: small-caps">BAM</font>)</h3>
<div class="outline-text-3" id="text-3-4">
<p>
<font style="font-variant: small-caps">GenMC</font> v0.6 comes with built-in support for <code>pthread_barrier_t</code>
functions (see Section <a href="#org017383e">5</a>) via <font style="font-variant: small-caps">BAM</font>.<sup>9</sup>
As an example of <font style="font-variant: small-caps">BAM</font> in action, consider the following program:
</p>

<div class="org-src-container">
<pre class="src src-C"><span style="color: #586e75; font-style: italic;">/* </span><span style="color: #586e75; font-style: italic;">file: bam.c</span><span style="color: #586e75; font-style: italic;"> */</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdio.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdlib.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;pthread.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdatomic.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;genmc.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;assert.h&gt;</span>

<span style="color: #d33682;">#if</span><span style="color: #d33682;">n</span><span style="color: #d33682;">def</span> N
<span style="color: #d33682;"># define</span> <span style="color: #6c71c4;">N</span> 2
<span style="color: #d33682;">#endif</span>

<span style="color: #268bd2;">pthread_barrier_t</span> <span style="color: #6c71c4;">b</span>;
<span style="color: #268bd2;">atomic_int</span> <span style="color: #6c71c4;">x</span>;

<span style="color: #268bd2;">void</span> *<span style="color: #b58900;">thread_n</span>(<span style="color: #268bd2;">void</span> *<span style="color: #6c71c4;">unused</span>)
{
        ++x;
        pthread_barrier_wait(&amp;b);
        assert(x == N);
        <span style="color: #859900;">return</span> <span style="color: #268bd2;">NULL</span>;
}

<span style="color: #268bd2;">int</span> <span style="color: #b58900;">main</span>()
{
        <span style="color: #268bd2;">pthread_t</span> <span style="color: #6c71c4;">t</span>[N];

        pthread_barrier_init(&amp;b, <span style="color: #268bd2;">NULL</span>, N);
        <span style="color: #859900;">for</span> (<span style="color: #268bd2;">int</span> <span style="color: #6c71c4;">i</span> = 0u; i &lt; N; i++) {
                <span style="color: #859900;">if</span> (pthread_create(&amp;t[i], <span style="color: #268bd2;">NULL</span>, thread_n, <span style="color: #268bd2;">NULL</span>))
                        abort();
        }

        <span style="color: #859900;">return</span> 0;
}
</pre>
</div>

<p>
Running <font style="font-variant: small-caps">GenMC</font> on the program above results in the following output:
</p>
<div class="org-src-container">
<pre class="src src-sh">Number of complete executions explored: 2
Total wall-clock time: 0.01s
</pre>
</div>
<p>
As can be seen, <font style="font-variant: small-caps">GenMC</font> treats <code>barrier_wait</code> calls as no-ops,
and they do not lead to any additional explorations. (The two executions
explored correspond to the possible ways in which <code>x</code> can be incremented).
</p>

<p>
However, if we disable <font style="font-variant: small-caps">BAM</font> by means of the <code>-disable-bam</code> switch,
get get the following output:
</p>
<div class="org-src-container">
<pre class="src src-sh">Number of complete executions explored: 4
Number of blocked executions seen: 4
Total wall-clock time: 0.01s
</pre>
</div>

<p>
Note that while <font style="font-variant: small-caps">BAM</font> can lead to the exploration of exponentially
fewer executions, it can only be used if the result of the <code>barrier_wait</code>
is not used. If it is, then using <code>-disable-bam</code> is necessary,
as <font style="font-variant: small-caps">GenMC</font> currently does not enforce this limitation.
</p>
</div>
</div>


<div id="outline-container-orgcc0984a" class="outline-3">
<h3 id="orgcc0984a"><span class="section-number-3">3.5</span> Symmetry Reduction</h3>
<div class="outline-text-3" id="text-3-5">
<p>
<font style="font-variant: small-caps">GenMC</font> also employs an experimental symmetry reduction mechanism.
While <font style="font-variant: small-caps">GenMC</font>'s symmetry reduction does not guarantee optimality,
i.e., might explore more executions than what an ideal symmetry
reduction algorithm would (although never more than what the enabled
partitioning dictates), it is still beneficial to use when threads
use the same code.
</p>

<p>
For instance, if <code>-sr</code> is used in the following program, <font style="font-variant: small-caps">GenMC</font>
explores only one execution instead of 6.
</p>
<div class="org-src-container">
<pre class="src src-C"><span style="color: #586e75; font-style: italic;">/* </span><span style="color: #586e75; font-style: italic;">file: sr.c</span><span style="color: #586e75; font-style: italic;"> */</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdio.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdlib.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;pthread.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdatomic.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;genmc.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;assert.h&gt;</span>

<span style="color: #268bd2;">atomic_int</span> <span style="color: #6c71c4;">x</span>;

<span style="color: #268bd2;">void</span> *<span style="color: #b58900;">thread_n</span>(<span style="color: #268bd2;">void</span> *<span style="color: #6c71c4;">unused</span>)
{
        ++x;
        <span style="color: #859900;">return</span> <span style="color: #268bd2;">NULL</span>;
}

<span style="color: #268bd2;">int</span> <span style="color: #b58900;">main</span>()
{
        <span style="color: #268bd2;">pthread_t</span> <span style="color: #6c71c4;">t1</span>, <span style="color: #6c71c4;">t2</span>, <span style="color: #6c71c4;">t3</span>;

        <span style="color: #859900;">if</span> (pthread_create(&amp;t1, <span style="color: #268bd2;">NULL</span>, thread_n, <span style="color: #268bd2;">NULL</span>))
                abort();
        <span style="color: #859900;">if</span> (pthread_create(&amp;t2, <span style="color: #268bd2;">NULL</span>, thread_n, <span style="color: #268bd2;">NULL</span>))
                abort();
        <span style="color: #859900;">if</span> (pthread_create(&amp;t3, <span style="color: #268bd2;">NULL</span>, thread_n, <span style="color: #268bd2;">NULL</span>))
                abort();

        <span style="color: #859900;">return</span> 0;
}
</pre>
</div>

<p>
In order for symmetry reduction to actually take place, the spawned
threads need to share exactly the same code, have exactly the same
arguments, and also there must not be any memory access (at the
LLVM-IR level) between the spawn instructions.
</p>
</div>
</div>


<div id="outline-container-org38f46c5" class="outline-3">
<h3 id="org38f46c5"><span class="section-number-3">3.6</span> Checking Liveness <a id="org7533b48"></a></h3>
<div class="outline-text-3" id="text-3-6">
<p>
<font style="font-variant: small-caps">GenMC</font> can also check for liveness violations in programs with
spinloops. Consider the following simple program:
</p>

<div class="org-src-container">
<pre class="src src-C"><span style="color: #586e75; font-style: italic;">/* </span><span style="color: #586e75; font-style: italic;">file: liveness.c</span><span style="color: #586e75; font-style: italic;"> */</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdlib.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;pthread.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdatomic.h&gt;</span>

<span style="color: #268bd2;">atomic_int</span> <span style="color: #6c71c4;">x</span>;

<span style="color: #268bd2;">void</span> *<span style="color: #b58900;">thread_1</span>(<span style="color: #268bd2;">void</span> *<span style="color: #6c71c4;">unused</span>)
{
        <span style="color: #859900;">while</span> (<span style="color: #268bd2;">!</span>x)
                ;
        <span style="color: #859900;">return</span> <span style="color: #268bd2;">NULL</span>;
}

<span style="color: #268bd2;">int</span> <span style="color: #b58900;">main</span>()
{
        <span style="color: #268bd2;">pthread_t</span> <span style="color: #6c71c4;">t1</span>;

        <span style="color: #859900;">if</span> (pthread_create(&amp;t1, <span style="color: #268bd2;">NULL</span>, thread_1, <span style="color: #268bd2;">NULL</span>))
                abort();

        <span style="color: #859900;">return</span> 0;
}
</pre>
</div>
<p>
Since there are no writes to \(x\), the loop in <code>thread_1</code> above
will never terminate. Indeed, running <font style="font-variant: small-caps">GenMC</font> with
 <code>-check-liveness</code> produces a relevant error report:
</p>
<div class="org-src-container">
<pre class="src src-sh">Error detected: Liveness violation!
<span style="color: #b58900;">Event</span> (1, 4) <span style="color: #859900;">in</span> graph:
&lt;-1, 0&gt; main:
        (0, 0): B
        (0, 1): TC [forks 1] L.19
        (0, 2): E
&lt;0, 1&gt; thread_1:
        (1, 0): B
        (1, 1): LOOP_BEGIN
        (1, 2): SPIN_START
        (1, 3): Rsc (x, 0) [INIT] L.9
        (1, 4): BLOCK [spinloop]

Non-terminating spinloop: thread 1
Number of complete executions explored: 0
Number of blocked executions seen: 1
Total wall-clock time: 0.07s
</pre>
</div>

<p>
The <code>-check-liveness</code> switch will automatically check for liveness
violations in all loops that have been captured by the spin-assume
transformation (see <a href="#org59fce12">4</a>).
</p>
</div>
</div>


<div id="outline-container-org9ed8a7b" class="outline-3">
<h3 id="org9ed8a7b"><span class="section-number-3">3.7</span> System Calls and Persistency Checks (<font style="font-variant: small-caps">Persevere</font>) <a id="org15bfc33"></a></h3>
<div class="outline-text-3" id="text-3-7">
<p>
Since v0.5, <font style="font-variant: small-caps">GenMC</font> supports the verification programs involving
system calls for file manipulation like <code>read()</code> and <code>write()</code>.  In
addition, using <font style="font-variant: small-caps">Persevere</font>,<sup>10</sup>
<font style="font-variant: small-caps">GenMC</font> can verify persistency properties of such programs. Below
we discuss some details that are important when it comes to verifying
programs that involve file manipulation.
</p>
</div>

<div id="outline-container-org326b97c" class="outline-4">
<h4 id="org326b97c"><span class="section-number-4">3.7.1</span> Consistency of File-Manipulating Programs</h4>
<div class="outline-text-4" id="text-3-7-1">
<p>
As a first example consider the program below, where a file
<code>"foo.txt"</code> is first populated by <code>main</code>, and then concurrently
read and written by two threads at offset 0:
</p>

<div class="org-src-container">
<pre class="src src-C"><span style="color: #586e75; font-style: italic;">/* </span><span style="color: #586e75; font-style: italic;">file: file-rw.c</span><span style="color: #586e75; font-style: italic;"> */</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdio.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdlib.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;unistd.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;fcntl.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdatomic.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;pthread.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;assert.h&gt;</span>

<span style="color: #268bd2;">void</span> *<span style="color: #b58900;">thread_1</span>(<span style="color: #268bd2;">void</span> *<span style="color: #6c71c4;">fdp</span>)
{
        <span style="color: #268bd2;">int</span> <span style="color: #6c71c4;">fd</span> = *((<span style="color: #268bd2;">int</span> *) fdp);
        <span style="color: #268bd2;">char</span> <span style="color: #6c71c4;">buf</span>[8];

        buf[0] = buf[1] = 1;
        <span style="color: #268bd2;">int</span> <span style="color: #6c71c4;">nw</span> = pwrite(fd, buf, 2, 0);
        <span style="color: #859900;">return</span> <span style="color: #268bd2;">NULL</span>;
}

<span style="color: #268bd2;">void</span> *<span style="color: #b58900;">thread_2</span>(<span style="color: #268bd2;">void</span> *<span style="color: #6c71c4;">fdp</span>)
{
        <span style="color: #268bd2;">int</span> <span style="color: #6c71c4;">fd</span> = *((<span style="color: #268bd2;">int</span> *) fdp);
        <span style="color: #268bd2;">char</span> <span style="color: #6c71c4;">buf</span>[8];

        <span style="color: #268bd2;">int</span> <span style="color: #6c71c4;">nr</span> = pread(fd, buf, 2, 0);
        <span style="color: #859900;">if</span> (nr == 2)
                assert((buf[0] == 0 &amp;&amp; buf[1] == 0) || (buf[0] == 1 &amp;&amp; buf[1] == 1));
        <span style="color: #859900;">return</span> <span style="color: #268bd2;">NULL</span>;
}

<span style="color: #268bd2;">int</span> <span style="color: #b58900;">main</span>()
{
        <span style="color: #268bd2;">pthread_t</span> <span style="color: #6c71c4;">t1</span>, <span style="color: #6c71c4;">t2</span>;
        <span style="color: #268bd2;">char</span> <span style="color: #6c71c4;">buf</span>[8];

        <span style="color: #268bd2;">int</span> <span style="color: #6c71c4;">fd</span> = open(<span style="color: #2aa198;">"foo.txt"</span>, O_CREAT|O_RDWR, 0);

        buf[0] = buf[1] = 0;
        <span style="color: #268bd2;">int</span> <span style="color: #6c71c4;">nw</span> = write(fd, buf, 2);
        assert(nw == 2);

        <span style="color: #859900;">if</span> (pthread_create(&amp;t1, <span style="color: #268bd2;">NULL</span>, thread_1, &amp;fd))
                abort();
        <span style="color: #859900;">if</span> (pthread_create(&amp;t2, <span style="color: #268bd2;">NULL</span>, thread_2, &amp;fd))
                abort();

        <span style="color: #859900;">if</span> (pthread_join(t1, <span style="color: #268bd2;">NULL</span>))
                abort();
        <span style="color: #859900;">if</span> (pthread_join(t2, <span style="color: #268bd2;">NULL</span>))
                abort();

        <span style="color: #859900;">return</span> 0;
}
</pre>
</div>

<p>
One property we might be interested in in the above program is whether
the reading thread can see any other (intermediate) state for the file
apart from <code>00</code> and <code>11</code>. Indeed, as can be seen below, running <font style="font-variant: small-caps">GenMC</font>
on the program above produces an example where the assertion is violated.
</p>
<div class="org-src-container">
<pre class="src src-sh">Error detected: Safety violation!
[...]
Assertion violation: (<span style="color: #6c71c4;">buf</span>[0] == 0 &amp;&amp; buf[1] == 0) || (buf[0] == 1 &amp;&amp; buf[1] == 1)
Number of complete executions explored: 1
Total wall-clock time: 0.03s
</pre>
</div>
<p>
Apart from safety violations like in this case, <font style="font-variant: small-caps">GenMC</font> will also
report system call failures as errors (e.g., trying to write to a file
that has been opened with <code>O_RDONLY</code>). This behavior can be disabled
with <code>-disable-stop-on-system-error</code>, which will make <font style="font-variant: small-caps">GenMC</font> report
such errors through <code>errno</code>.
</p>

<p>
When including headers like <code>stdio.h</code> or <code>unistd.h</code>, <font style="font-variant: small-caps">GenMC</font> intercepts
calls to <code>open()</code>, <code>read()</code>, <code>write()</code>, and other system calls defined
in these header files, and models their behavior. Note that these header
files are also part of <font style="font-variant: small-caps">GenMC</font> so, in general, only the functionality
described in Section <a href="#org017383e">5</a> from said header files can be used in programs.
</p>

<p>
Note that only constant (static) strings can be used as filenames when
using system calls. The filenames need not exist as regular files in
the user's system, as the effects of these system calls are modeled,
and not actually executed. Thus, it is in general preferable if the
contents of the manipulated files maintain a small size across
executions.
</p>
</div>
</div>

<div id="outline-container-orgc48d708" class="outline-4">
<h4 id="orgc48d708"><span class="section-number-4">3.7.2</span> Persistency of File-Manipulating Programs</h4>
<div class="outline-text-4" id="text-3-7-2">
<p>
In addition to checking whether safety properties of file-manipulating
programs with regards to consistency are satisfied (as described
above), <font style="font-variant: small-caps">GenMC</font> can also check whether some safety property with
regards to persistency (under <code>ext4</code>) is satisfied.  This is achieved
through <font style="font-variant: small-caps">Persevere</font>, which can be enabled with <code>-persevere</code>.
</p>

<p>
For example, let us consider the program below and suppose we want to
check whether, after a crash, it is possible to observe only a part of
an append to a file:
</p>

<div class="org-src-container">
<pre class="src src-C"><span style="color: #586e75; font-style: italic;">/* </span><span style="color: #586e75; font-style: italic;">file: pers.c</span><span style="color: #586e75; font-style: italic;"> */</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdio.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdlib.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;unistd.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;stdatomic.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;pthread.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;assert.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;genmc.h&gt;</span>

<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;fcntl.h&gt;</span>
<span style="color: #d33682;">#include</span> <span style="color: #2aa198;">&lt;sys/stat.h&gt;</span>

<span style="color: #268bd2;">void</span> <span style="color: #b58900;">__VERIFIER_recovery_routine</span>(<span style="color: #268bd2;">void</span>)
{
        <span style="color: #268bd2;">char</span> <span style="color: #6c71c4;">buf</span>[8];
        buf[0] = 0;
        buf[1] = 0;

        <span style="color: #268bd2;">int</span> <span style="color: #6c71c4;">fd</span> = open(<span style="color: #2aa198;">"foo.txt"</span>, O_RDONLY, 0666);
        assert(fd != -1);

        <span style="color: #586e75; font-style: italic;">/* </span><span style="color: #586e75; font-style: italic;">Is is possible to read something other than {2,2} ?</span><span style="color: #586e75; font-style: italic;"> */</span>
        <span style="color: #268bd2;">int</span> <span style="color: #6c71c4;">nr</span> = pread(fd, buf, 2, 3);
        <span style="color: #859900;">if</span> (nr == 2)
                assert(buf[0] == 2 &amp;&amp; buf[1] == 2);
        <span style="color: #859900;">return</span>;
}

<span style="color: #268bd2;">int</span> <span style="color: #b58900;">main</span>()
{
        <span style="color: #268bd2;">char</span> <span style="color: #6c71c4;">buf</span>[8];

        buf[0] = 1;
        buf[1] = 1;
        buf[2] = 1;

        <span style="color: #268bd2;">int</span> <span style="color: #6c71c4;">fd</span> = open(<span style="color: #2aa198;">"foo.txt"</span>, O_CREAT|O_TRUNC|O_RDWR, S_IRWXU);
        write(fd, buf, 3);

        __VERIFIER_pbarrier();

        write(fd, buf + 3, 2);

        close(fd);

        <span style="color: #859900;">return</span> 0;
}
</pre>
</div>

<p>
In the program above, the <code>__VERIFIER_pbarrier()</code> call ensures that
all the file operations before it will be considered as "persisted"
(i.e., having reached disk) in this program. The function
<code>__VERIFIER_recovery_routine()</code> is automatically called by <font style="font-variant: small-caps">GenMC</font>
and contains the code to be run by the recovery routine, in order to
observe the post-crash disk state.
</p>

<p>
In this case, by issuing <code>genmc -persevere pers.c</code> we observe that
partly observing the append is indeed possible under <code>ext4</code>, as can
be seen below.
</p>
<div class="org-src-container">
<pre class="src src-sh">Error detected: Recovery error!
[...]
Assertion violation: <span style="color: #6c71c4;">buf</span>[0] == 2 &amp;&amp; buf[1] == 2
Number of complete executions explored: 2
Total wall-clock time: 0.08s
</pre>
</div>
<p>
For this program in particular, this property is violated due to the
default block size (which is 2 bytes), and the nature of appends in
the default data ordering mode of <code>ext4</code> (<code>data=ordered</code>).
</p>

<p>
In general, such parameters of <code>ext4</code> can be tuned via the
<code>--block-size</code> and <code>--journal-data</code> switches (see Section <a href="#org59fce12">4</a> and
<code>genmc -help</code> for more information).  <font style="font-variant: small-caps">GenMC</font> currently assumes a
sector size of 1 byte.
</p>
</div>
</div>
</div>
</div>


<div id="outline-container-org2085b6d" class="outline-2">
<h2 id="org2085b6d"><span class="section-number-2">4</span> Command-line Options <a id="org59fce12"></a></h2>
<div class="outline-text-2" id="text-4">
<p>
A full list of the available command-line options can by viewed
by issuing <code>genmc -help</code>. Below we describe the ones that
are most useful when verifying user programs.
</p>

<dl class="org-dl">
<dt><code>-rc11</code></dt><dd>Perform the exploration under the RC11 memory model (default)</dd>
<dt><code>-imm</code></dt><dd>Perform the exploration under the IMM memory model</dd>
<dt><code>-lkmm</code></dt><dd>Perform the exploration under the LKMM memory model (experimental)</dd>
<dt><code>-wb</code></dt><dd>Perform the exploration based on the <span style="color: #808080; font-family: monospace">po</span><span style="color: #00ff00; font-family: monospace">rf</span>
equivalence partitioning.</dd>
<dt><code>-mo</code></dt><dd>Perform the exploration based on the <span style="color: #808080; font-family: monospace">po</span> \(\cup\) <span style="color: #00ff00; font-family: monospace">rf</span> \(\cup\) <span style="color: #ffa500; font-family: monospace">mo</span>
equivalence partitioning (default).</dd>
<dt><code>-lapor</code></dt><dd>Enable Lock-Aware Partial Order Reduction (<font style="font-variant: small-caps">LAPOR</font>)</dd>
<dt><code>-disable-bam</code></dt><dd>Disables Barrier-Aware Model-checking (<font style="font-variant: small-caps">BAM</font>)</dd>
<dt><code>-check-liveness</code></dt><dd>Check for liveness violations in spinloops</dd>
<dt><code>-persevere</code></dt><dd>Enable <code>ext4</code> persistency checks (<font style="font-variant: small-caps">Persevere</font>)</dd>
<dt><code>-unroll=&lt;N&gt;</code></dt><dd>All loops will be executed at most \(N\) times.</dd>
<dt><code>-dump-error-graph=&lt;file&gt;</code></dt><dd>Outputs an erroneous graph to file
<code>&lt;file&gt;</code>.</dd>
<dt><code>-print-error-trace</code></dt><dd>Outputs a sequence of source-code instructions
that lead to an error.</dd>
<dt><code>-disable-race-detection</code></dt><dd>Disables race detection for non-atomic
accesses.</dd>
<dt><code>-program-entry-function=&lt;fun_name&gt;</code></dt><dd>Uses function <code>&lt;fun_name&gt;</code>
as the program's entry point, instead of <code>main()</code>.</dd>
<dt><code>-disable-spin-assume</code></dt><dd>Disables the transformation of spin loops to
<code>assume()</code> statements.</dd>
</dl>
</div>
</div>


<div id="outline-container-orgdc94ef2" class="outline-2">
<h2 id="orgdc94ef2"><span class="section-number-2">5</span> Supported APIs <a id="org017383e"></a></h2>
<div class="outline-text-2" id="text-5">
<p>
Apart from C11 API (defined in <code>stdatomic.h</code>) and the <code>assert()</code>
function used to define safety specifications, below we list supported
functions from different libraries.
</p>
</div>

<div id="outline-container-orgc4fffed" class="outline-3">
<h3 id="orgc4fffed"><span class="section-number-3">5.1</span> Supported <code>stdio</code>, <code>unistd</code> and <code>fcntl</code> API</h3>
<div class="outline-text-3" id="text-5-1">
<p>
The following functions are supported for I/O:
</p>

<dl class="org-dl">
<dt><code>int printf(const char *, ...)</code></dt><dd></dd>

<dt><code>int open (const char *, int , mode_t)</code></dt><dd></dd>

<dt><code>int creat (const char *, mode_t)</code></dt><dd></dd>

<dt><code>off_t lseek (int, off_t, int)</code></dt><dd></dd>

<dt><code>int close (int)</code></dt><dd></dd>

<dt><code>ssize_t read (int, void *, size_t)</code></dt><dd></dd>

<dt><code>ssize_t write (int, const void *, size_t)</code></dt><dd></dd>

<dt><code>ssize_t pread (int, void *, size_t, off_t)</code></dt><dd></dd>

<dt><code>ssize_t pwrite (int, const void *, size_t, off_t)</code></dt><dd></dd>

<dt><code>int truncate (const char *, off_t)</code></dt><dd></dd>

<dt><code>int link (const char *, const char *)</code></dt><dd></dd>

<dt><code>int unlink (const char *)</code></dt><dd></dd>

<dt><code>int rename (const char *, const char *)</code></dt><dd></dd>

<dt><code>int fsync (int)</code></dt><dd></dd>

<dt><code>void sync (void)</code></dt><dd></dd>
</dl>

<p>
Note that the functions above are modeled and not actually executed,
as described in Section <a href="#org15bfc33">3.7</a>.
</p>
</div>
</div>

<div id="outline-container-org6f8044c" class="outline-3">
<h3 id="org6f8044c"><span class="section-number-3">5.2</span> Supported <code>stdlib</code> API</h3>
<div class="outline-text-3" id="text-5-2">
<p>
The following functions are supported from <code>stdlib.h</code>:
</p>

<dl class="org-dl">
<dt><code>void abort(void)</code></dt><dd></dd>

<dt><code>int abs(int)</code></dt><dd></dd>

<dt><code>int atoi(const char *)</code></dt><dd></dd>

<dt><code>void free(void *)</code></dt><dd></dd>

<dt><code>void *malloc(size_t)</code></dt><dd></dd>

<dt><code>void *aligned_alloc(size_t, size_t)</code></dt><dd></dd>
</dl>
</div>
</div>

<div id="outline-container-org0afb1fd" class="outline-3">
<h3 id="org0afb1fd"><span class="section-number-3">5.3</span> Supported <code>pthread</code> API</h3>
<div class="outline-text-3" id="text-5-3">
<p>
The following functions are supported from <code>pthread.h</code>:
</p>

<dl class="org-dl">
<dt><code>int pthread_create (pthread_t *, const pthread_attr_t *, void *(*) (void *), void *)</code></dt><dd></dd>

<dt><code>int pthread_join (pthread_t, void **)</code></dt><dd></dd>

<dt><code>pthread_t pthread_self (void)</code></dt><dd></dd>

<dt><code>void pthread_exit (void *)</code></dt><dd></dd>

<dt><code>int pthread_mutex_init (pthread_mutex_t *, const pthread_mutexattr_t *)</code></dt><dd></dd>

<dt><code>int pthread_mutex_lock (pthread_mutex_t *)</code></dt><dd></dd>

<dt><code>int pthread_mutex_trylock (pthread_mutex_t *)</code></dt><dd></dd>

<dt><code>int pthread_mutex_unlock (pthread_mutex_t *)</code></dt><dd></dd>

<dt><code>int pthread_mutex_destroy (pthread_mutex_t *)</code></dt><dd></dd>

<dt><code>int pthread_barrier_init (pthread_barrier_t *, const pthread_barrierattr_t *, unsigned)</code></dt><dd></dd>

<dt><code>int pthread_barrier_wait (pthread_barrier_t *)</code></dt><dd></dd>

<dt><code>int pthread_barrier_destroy (pthread_barrier_t *)</code></dt><dd></dd>
</dl>
</div>
</div>


<div id="outline-container-org211066f" class="outline-3">
<h3 id="org211066f"><span class="section-number-3">5.4</span> Supported SV-COMP<sup>6</sup> API</h3>
<div class="outline-text-3" id="text-5-4">
<p>
The following functions from the ones defined in SV-COMP<sup>6</sup> are supported:
</p>

<dl class="org-dl">
<dt><code>void __VERIFIER_assume(int)</code></dt><dd></dd>

<dt><code>int __VERIFIER_nondet_int(void)</code></dt><dd></dd>
</dl>

<p>
Note that, since <font style="font-variant: small-caps">GenMC</font> is a stateless model checker, <code>__VERIFIER_nondet_int()</code>
only "simulates" data non-determism, and does actually provide support for it.
More specifically, the sequence of numbers it produces for each thread, remains
the same across different executions.
</p>
</div>
</div>
</div>

<div id="outline-container-orgb713789" class="outline-2">
<h2 id="orgb713789"><span class="section-number-2">6</span> Contact <a id="org5e4410b"></a></h2>
<div class="outline-text-2" id="text-6">
<p>
For feedback, questions, and bug reports please send an e-mail to
<a href="mailto:michalis@mpi-sws.org">michalis@mpi-sws.org</a>.
</p>
</div>
</div>

<div id="outline-container-orgb780d83" class="outline-2">
<h2 id="orgb780d83"><span class="section-number-2">7</span> Bibliography <a id="orgc6d0654"></a></h2>
<div class="outline-text-2" id="text-7">
<ol class="org-ol">
<li>Lahav,  Ori; Vafeiadis,  Viktor; Kang,  Jeehoon; Hur,  Chung-Kil and Dreyer,  Derek, <i>Repairing sequential consistency in {C/C++11}</i>, PLDI 2017(2017). <br></li>
<li>Podkopaev,  Anton; Lahav,  Ori and Vafeiadis,  Viktor, <i>Bridging the gap between programming languages and hardware weak memory models</i>, Proc. ACM Program. Lang., 3<b>(POPL)</b>, pp. 69:1&#x2013;69:31 (2019). <a href="http://dx.doi.org/10.1145/3290382">http://dx.doi.org/10.1145/3290382</a>. <br></li>
<li>Alglave,  Jade; Maranget,  Luc; McKenney,  Paul E.; Parri,  Andrea and Stern,  Alan, <i>Frightening small children and disconcerting grown-ups: {Concurrency} in the Linux kernel</i>, ASPLOS 2018(2018). <br></li>
<li>Kokologiannakis,  Michalis; Raad,  Azalea and Vafeiadis,  Viktor, <i>Model checking for weakly consistent libraries</i>, PLDI 2019(2019). <br></li>
<li>Kokologiannakis,  Michalis; Marmanis,  Iason; Gladstein,  Vladimir and Vafeiadis,  Viktor, <i>Truly stateless, optimal dynamic partial order reduction</i>, Proc. ACM Program. Lang., 6<b>(POPL)</b>, pp.  (2022). <a href="http://dx.doi.org/10.1145/3498711">http://dx.doi.org/10.1145/3498711</a>. <br></li>
<li>SV-COMP, , <i>Competition on Software Verification ({SV-COMP})</i>,  <a href="http://dx.doi.org/https://sv-comp.sosy-lab.org/2019/">http://dx.doi.org/https://sv-comp.sosy-lab.org/2019/</a>. <a href="http://dx.doi.org/nil">http://dx.doi.org/nil</a>. <br></li>
<li>Kokologiannakis, Michalis; Ren, Xiaowei and Vafeiadis, Viktor, <i>Dynamic Partial Order Reductions for Spinloops</i>, FMCAD 2021(2021). <br></li>
<li>Kokologiannakis,  Michalis; Raad,  Azalea and Vafeiadis,  Viktor, <i>Effective lock handling in stateless model checking</i>, Proc. ACM Program. Lang., 3<b>(OOPSLA)</b>, pp.  (2019). <a href="http://dx.doi.org/10.1145/3360599">http://dx.doi.org/10.1145/3360599</a>. <br></li>
<li>Kokologiannakis,  Michalis and Vafeiadis,  Viktor, <i>{BAM}: {Efficient} Model Checking for Barriers</i>, NETYS 2021(2021). <br></li>
<li>Kokologiannakis,  Michalis; Kaysin,  Ilya; Raad,  Azalea and Vafeiadis,  Viktor, <i>{PerSeVerE}: {Persistency} semantics for verification under ext4</i>, Proc. ACM Program. Lang., 5<b>(POPL)</b>, pp.  (2021). <a href="http://dx.doi.org/10.1145/3434324">http://dx.doi.org/10.1145/3434324</a>.</li>
</ol>
</div>
</div>
</div>
<div id="postamble" class="status">
<p class="date">Created: 2022-02-22 Tue 22:32</p>
<p class="validation"><a href="http://validator.w3.org/check?uri=referer">Validate</a></p>
</div>
</body>
</html>
