flows-infer

Inferring local invariants for the flow framework using horn clauses.

node_insert.hcc contains a non-deterministic list insertion example encoded in Tricera. To run, download and install Tricera from the Github repository, then call:

./tri ../flows-infer/node.hcc

node_insert_delete.c uses C macros to redefine the flow. To test it, run: gcc -E -CC ./node_insert_delete.c -o ./node_insert_delete.hcc tri ./node_insert_delete.hcc

However, currently node_insert_delete.c is taking upwards of 10 minutes to run.

Link to Overleaf document: https://www.overleaf.com/project/62190ca137d115527f7f97bf

Instrumentation / triceratops

The code instrumentation is automated in the Python tool triceratops.

Requirements

To run triceratops, you need Python 3 (>= 3.10; 3.12 recommended) as well as the dependencies listed in requirements.txt. You can install the dependencies using pip:

  pip install -r triceratops/requirements.txt

Optional: You may wish to use a virtual environment to not pollute your system. First, initialize the virtual environment:

  python3 -m venv venv
  source venv/bin/activate
  pip install -r triceratops/requirements.txt

Then, before running triceratops, enter the virtual environment whenever you open a new shell:

  source venv/bin/activate

Running

To run triceratops, just invoke it from the root of this repository like so:

  python3 triceratops <input> [-o output] [-f] [-s] [--tri] [--concise]

The input may be a file with extension .c or a folder. If a folder is given, all .c files it contains are instrumented. The output is a file or a folder. If the input is file.c then the output can be omitted and file.hcc is used instead. If the input is a folder, the output must be provided and must be a folder as well. The remaining flags have the following meaning:

• -f: instructs the tool to overwrite existing files; by default existing files are not overwritten.
• -s: suppresses most output (in particular tricera output); by default triceratops is chatty.
• --tri: verifies the instrumentation by running tricera on it; requires the input to be a file.
  Note: you must provide the proper path to the tricera executable in __main__.py (see TRICERA_EXEC)
• --concise: removes the explanation comments from the instrumentation.

You can also run triceratops from the sub-folder:

  python3 __main__.py <input> [-o output] [-f]  # or
  python3 . <input> [-o output] [-f]

The instrumentation (output files) produced by triceratops is compatible with the run_experiment.sh and benchmark.sh scripts discussed below.

Input Flags

In addition to command line flags, there are the following flags that can be added to input .c files to configure the instrumentation. The flags are added by #define FLAG statements at the beginning of each file.

Flag	Meaning
PHYSICAL	Enforces the heap graph to be acyclic. This is the most stringent setting.
MIXED	Enforces the flow to be acyclic, but will do so by enforcing the heap graph of footprints to be physically acyclic.
EFFECTIVE	Enforces the flow to be acyclic. This is the most relaxed setting.
SEQUENTIAL	Assumes the program is sequential.
COOP	Assumes the program is concurrent and that all interferences are appropriately annotated with yield instructions.
PREEMPTIVE	Assumes the program is concurrent and will add the necessary yield instructions enforcing a one-lock-per-object locking strategy.
EXPECTED_TRUE	Indicates that the input program is expected to be safe.
EXPECTED_FALSE	Indicates that the input program is expected to be unsafe.

How to Run

There is a bash script that automates the process of running Tricera on .c or .hcc files called run_experiment.sh. It aids in the execution and logging of Tricera on examples, by creating unique folders based on timestamps (and optional tags), copying necessary files, executing Tricera with both default and user-provided arguments, and logging the output. It also calls the C preprocessor on any input .c files before passing it to Tricera.

Features:

• Unique Folder Creation: For each run, the script creates a unique folder named based on the current date and time. An optional tag can also be appended to the folder's name for better identification.

• File Management: The input source file is copied into the newly created folder to keep track of the exact version of the file used for the run.

• C Preprocessor: The script calls the C preprocessor on the input .c file before passing it to Tricera. This allows the user to use macros in the input file.

• Detailed Logging: All outputs (including errors) of the Tricera program are logged into a log file within the run's folder. The log file also captures details like date, time, and filename at the beginning of each run.

• Flexible Command Invocation: The script supports passing additional arguments to TRICERA. These arguments are appended after the default arguments defined within the script.

Configuration

At the top of the script, there are several user-configurable variables:

• TARGET_DIR: Defines the base directory where the unique run folders will be created. By default, this should point to the executions folder in this repository.
• TRICERA: Path to the Tricera executable.
• DEFAULT_ARGS: A string containing default arguments passed to Tricera during every run.

Usage

./run_experiment [optional_tag] input_file [additional_tricera_args...]

optional_tag: An optional string that can be used to tag a specific run. If provided, this tag is appended to the unique folder's name. This parameter is optional and should not be a valid filename. input_file: This should be a .c or a .hcc source file you wish to process with Tricera. additional_TRICERA_args: Any additional arguments you want to pass to Tricera.

Example

If one wants to process a file named example.c and tag this run as "experiment_1", while also passing -flag1 and -flag2 to Tricera, the following commands should be used:

./run_experiment experiment_1 example.c -flag1 -flag2

or

./run_experiment "experiment 1" example.c -flag1 -flag2

or

./run_experiment example.c -flag1 -flag2

Benchmarking

To compare the runtime of multiple implementations use the benchmark script like so:

./benchmark 1 7 example.c other.c even.c more.c

The first two positional arguments are the number of warmups and the number of runs to average across. These arguments are optional, so you may simply do:

./benchmark example.c other.c

or to just specify the number of runs:

./benchmark 77 example.c other.c

The benchmark script requires Hyperfine to be installed.

Heap Size

Increase the JVM memory like this:

export JAVA_OPTS=-Xmx4g

Examples

See folder examples for more information.