Veracity2G

Veracity2G (V2G) parallelizes sequential programs by exploiting the commutativity of named commutative blocks (NCBs).

An NCB gives a name to a region of code, such as a loop body or a block in main. A commutativity { } prelude specifies the conditions under which instances of these regions commute. V2G can then verify these conditions, transform the program into parallel tasks, synthesize locks, and execute the result on a multicore runtime.

The source code is available on GitHub: https://github.com/veracity-lang/veracity2g.

Quick Start

The provided artifact VM already contains the required dependencies and configuration. From the repository root, run:

make

This builds the vcy executable in the repository root.

For VM setup and environment details, see the VM README included with the artifact.

The following example uses:

benchmarks/ncb/motivation.vcy

The benchmark contains two named blocks, f1 and f2, inside a loop. Its commutativity condition is:

commutativity {
    {f1(i_1, x, arr)}, {f2(i_2, arr)}:
        ((i_1 != i_2) || (i_1 == i_2 && arr[i_1] > 0))
}

The condition states that an f1 instance and an f2 instance commute when they operate on different indices, or when they operate on the same index and arr[i_1] > 0.

Quick workflow

After building, the main workflow can be run with:

# 1. Verify the commutativity condition
./vcy verify benchmarks/ncb/motivation.vcy --prover cvc5

# 2. Run sequentially
./vcy interp benchmarks/ncb/motivation.vcy 100 10

# 3. Run in parallel with synthesized locks
./vcy interp --dswp --synthesize-locks benchmarks/ncb/motivation.vcy 100 10

# 4. Optionally infer the commutativity condition (You need to remove the condition first and replace it with _)
./vcy infer benchmarks/ncb/motivation.vcy --prover cvc5 --poke2 --timeout=30

The two arguments 100 10 are passed to main as argv:

• 100 is the scalingfactor.
• 10 is the size of the output array.

The sequential and parallel executions should produce the same return value.

The three main commands are described in more detail below.

1. Verify

Check that the commutativity condition is sound:

./vcy verify benchmarks/ncb/motivation.vcy --prover cvc5

The result reports whether the condition is correct, incorrect, or could not be verified.

An unsound condition can allow non-commuting blocks to execute concurrently, so conditions should be verified before parallel execution.

2. Interpret

Run the benchmark sequentially:

./vcy interp benchmarks/ncb/motivation.vcy 100 10

Then run it using the task-parallel execution model:

./vcy interp \
    --dswp \
    --synthesize-locks \
    benchmarks/ncb/motivation.vcy 100 10

With --dswp, V2G constructs parallel tasks and executes them using the commutativity-aware scheduler. --synthesize-locks inserts fine-grained locks where necessary.

The program prints:

Return: N

where N is the return value of main.

Lock synthesis operates on the parallel tasks produced by the DSWP transformation, not on the sequential program, so --synthesize-locks is always used together with --dswp.

To see the synchronization that V2G generates for the tasks, add --codegen:

./vcy interp --dswp --synthesize-locks benchmarks/ncb/commset.vcy --codegen

This writes the generated C code to /tmp/autogen_tasks.c, where you can inspect the semaphores (sem_t, sem_init, sem_wait, sem_post) generated to enforce the dependencies between tasks.

3. Infer

V2G can also infer a commutativity condition. Replace the explicit condition in motivation.vcy with _:

commutativity {
    {f1(i_1, x, arr)}, {f2(i_2, arr)}: _
}

Then run:

./vcy infer benchmarks/ncb/motivation.vcy --prover cvc5

Inference is experimental and may time out on larger blocks. Writing a condition explicitly and verifying it is the recommended workflow.

---

Detailed Documentation

Named Commutative Blocks

A named commutative block gives a name to a region of code and can optionally specify input variables:

label(x, y): { ... }

label: { ... }

The parameters are not function arguments. They identify local variables whose values at block entry can be referenced by the commutativity condition.

When the program is executed sequentially, the labels have no effect.

The commutativity prelude

At the top of a program, NCB pairs and their conditions are specified in a commutativity block:

commutativity {
    {f(i_1, arr)}, {g(i_2, arr)} :
        (i_1 != i_2 || (i_1 == i_2 && arr[i_1] > 0));

    {f(i_1, arr)}, {f(i_2, arr)} :
        (i_1 != i_2);

    {g(i_1, arr)}, {g(i_2, arr)} :
        (i_1 != i_2)
}

Important rules:

• Entries are separated by ;.
• Parameters are matched to block parameters by position.
• Names such as i_1 and i_2 are aliases used in the condition.
• Different aliases should be used when comparing two instances of the same NCB.
• The condition is a pure boolean expression over NCB inputs and global state.
• Conditions may use constants, arithmetic, comparisons, boolean operators, array reads, struct field reads, and read-only hashtable operations.
• Use true when two blocks always commute.
• Use _ to request condition inference.
• Pairs that are not listed are assumed not to commute.

At runtime, the scheduler evaluates the condition using the shared global state and the input values of the two jobs.

Commands

The general command-line form is:

./vcy <command> [flags] <program.vcy> [program args]

verify

Verify explicit commutativity conditions:

./vcy verify benchmarks/ncb/banking.vcy --prover cvc5

Useful options include:

Flag	Description
-q	Print only correct / incorrect
--cond	Print each condition
--html	Generate an HTML verification report
--htmlopen	Generate and open an HTML report
-ae	Required when the program uses havoc

infer

Infer conditions for NCBs whose condition is _:

./vcy infer benchmarks/ncb/other/vote-infer.vcy --prover cvc5

Inference can be limited with:

./vcy infer program.vcy --prover cvc5 --timeout N

parse

Parse and inspect a program:

./vcy parse --pretty program.vcy

interp

Run a program sequentially:

./vcy interp program.vcy ARGS

Run it using task parallelism:

./vcy interp --dswp program.vcy ARGS

Run it with synthesized locks:

./vcy interp --dswp --synthesize-locks program.vcy ARGS

Important options:

Flag	Description
--dswp	Enable task-parallel execution
--threads N	Worker pool size; default is 8
--synthesize-locks	Insert fine-grained locks
--emit-tasks	Print generated task bodies and exit
--codegen	Write generated C to /tmp/autogen_tasks.c
--html / --htmlopen	Generate a PDG, SCC DAG, and task-graph report
--time	Print execution time
--force-sequential	Disable parallel execution
--out-dir DIR	Specify the output directory

To inspect generated tasks without executing them:

./vcy interp --dswp --synthesize-locks --emit-tasks program.vcy ARGS

NCB Benchmarks

NCB examples are located in benchmarks/ncb/.

Benchmark	Illustrates	Example arguments
test/ncb_dot_product.vcy	Self-commuting loop body and synthesized reduction lock	4
test/ncb_histogram.vcy	(true) condition and shared bucket update	8
other/ncb_max_reduce.vcy	Max-reduction pattern	10
motivation.vcy	Paper running example with conditional commutativity	100 10
banking.vcy	Deposits, withdrawals, and transfers on distinct accounts	1 100 1000
erc20.vcy	ERC20 transfers	1 1 2
vote.vcy	Smart-contract voting	1
multi-blocks.vcy	Multiple NCBs and hashtable conditions	1
simple-io.vcy	Commutativity involving file I/O	Four file paths
commset.vcy	Benchmark adapted from CommSet	See scripts/run_tests.sh
commset-kmeans.vcy	Benchmark adapted from CommSet	See scripts/run_tests.sh
commset-potrace.vcy	Benchmark adapted from CommSet	See scripts/run_tests.sh
other/sollve_dotprod.vcy	Benchmark adapted from PS-DSWP / SOLLVE	1
other/simple-vector.vcy	Benchmark adapted from PS-DSWP / SOLLVE	1
other/2d-array.vcy	Benchmark adapted from PS-DSWP / SOLLVE	1

Building

When using the provided artifact VM, no dependency installation or environment configuration is required. Run:

make

For VM installation and environment setup, see the VM README.

When building outside the provided VM, V2G requires OCaml 5, OPAM, Dune, domainslib, and the other OCaml dependencies used by the project. V2G also uses Servois2 for SMT queries and requires at least one supported SMT solver.

CVC5 is the recommended solver. Z3 and Yices are also supported:

./vcy verify program.vcy --prover z3
./vcy verify program.vcy --prover yices

Testing

Run the complete test suite:

make test

Run the NCB benchmark and lock-synthesis tests:

bash scripts/run_tests.sh

Original Veracity commute Blocks

V2G also supports the original Veracity constructs, which reason about sequentially composed blocks:

commute _ {
    { block_A }
    { block_B }
}

commute (x > 0) {
    { block_A }
    { block_B }
}

Mover variants include:

commute_left
commute_right
commute_left_ctx <ctx>
commute_right_ctx <ctx>

Related commands are:

Command	Description
infer	Infer conditions for commute _ blocks
verify	Verify explicit conditions
invariants	Check that annotated loop invariants are inductive
assertions	Check assert() statements
translate	Translate to C

Examples:

./vcy infer benchmarks/prepost/pre.vcy --prover cvc5
./vcy verify benchmarks/verify/even-odd.vcy --prover cvc5
./vcy verify benchmarks/loops/scan.vcy --prover cvc5
./vcy invariants benchmarks/invariants/inc.vcy --prover cvc5
./vcy assertions benchmarks/vcgen/assert.vcy --prover cvc5

Loop invariants

When a commute block contains a loop, annotate it with an invariant:

while (i < n) invariant i >= 0 && i <= n {
    i = i + 1;
}

The invariant is used by the SMT encoding to represent the loop's net effect. Check that an invariant is inductive with:

./vcy invariants benchmarks/invariants/inc.vcy --prover cvc5

Loop support

Loops inside a block being verified are supported in one of three ways:

1. User-provided loop invariants. A while loop annotated with an invariant is encoded by its invariant, as described above.
2. Unrolling. A while loop that iterates a constant number of times (a counter initialized to a literal, compared against a literal bound, and incremented by a constant) is replaced by that many copies of its body. Unrolling is exact. Examples are in benchmarks/loop-unroll/.
3. Per-iteration commutativity. When the loop body does not depend on the loop counter, and each iteration commutes with the body of another NCB, verify checks a single iteration against the other block. By induction on swaps, the whole loop then commutes with that block. Examples are in benchmarks/loop-abstract/.

Any other loop is rejected with an error rather than being encoded unsoundly. Commutativity of general loops is an open problem and is left for future work.

Quantified conditions

A commute condition may use forall or exists:

commute (forall k : int . a[k] == 0) {
    ...
}

Quantified conditions are supported by verify. They are not generated by inference and cannot be executed by interp.

Reading Verification Counterexamples

When verify rejects a condition and --html is provided, Veracity writes an expr_table.html file into the corresponding report directory.

The table maps program expressions to their SMT values before and after each block execution. A counterexample is a state in which the two execution orders produce different final states.

Repository Layout

Path	Contents
benchmarks/ncb/	NCB programs
benchmarks/lock_synth/	Lock-synthesis tests
benchmarks/inferred/, verify/, loops/, …	Original Veracity benchmarks
scripts/	Test and task-generation scripts
reports/	Speedup and inference/verification scripts and plots
src/vcy/	Lexer, parser, interpreter, and CLI
src/analysis/	Servois2 translation, PDG, and task construction
src/parallel/	Multicore and single-core runtime backends
src/api/	Programmatic OCaml API
src/test/	OUnit2 test suites

OCaml API

The functionality is also available programmatically through Vcy.Veracity.

See API.md.