Skip to main content

Parallelism (--cores)

Run verification with multiple parallel worker threads.

Syntax​

sector9 --verify --cores <n> file.sr9

The <n> parameter specifies the number of parallel verification threads. This maps to Silicon's --numberOfParallelVerifiers flag with the value n-1.

Normal sector9 --verify runs default to one coordinating verifier thread unless you pass --cores. The raw VPR helper scripts/verify-vpr.sh defaults to one Silicon verifier worker explicitly so emitted-VPR timing comparisons are stable. Override that helper with VERIFY_VPR_PARALLEL_VERIFIERS=N when you are intentionally measuring raw Silicon worker scaling.

Examples​

# Use 4 cores (3 parallel verifiers + 1 main thread)
sector9 --verify --cores 4 file.sr9

# Use 8 cores for larger programs
sector9 --verify --cores 8 file.sr9

# Single-threaded verification (default)
sector9 --verify file.sr9

# Combine with timeout for CI
sector9 --verify --cores 4 --verify-timeout-ms 60000 file.sr9

How It Works​

The --cores N flag controls Silicon's internal parallelization:

  1. Thread allocation: Silicon spawns N-1 additional verifier threads beyond the main thread
  2. Method-level parallelism: Each verifier thread can work on a different method's proof obligations
  3. Backend scheduling: Silicon schedules independent obligations across those workers and invokes Z3 as needed

For example, --cores 4 results in 3 additional workers plus the main thread, giving 4 total verification threads.

When Parallelism Helps​

Parallelism provides the most benefit when:

  • Multiple methods: Programs with several independent methods can verify in parallel
  • Independent obligations: Methods with separate proof obligations benefit from concurrent solving
  • Balanced workloads: Methods with similar verification complexity maximize throughput

Parallelism provides limited benefit when:

  • Single method: One large method cannot be parallelized internally
  • Quantifier-heavy code: Complex forall/exists patterns bottleneck on SMT solving
  • Dependency chains: Methods that depend on each other's specifications
ScenarioCoresNotes
Development2-4Fast feedback during iteration
Multiple methods4-8Match available CPU cores
CI pipelines4Balance speed and resource usage
Resource-constrained1-2Minimize memory overhead

Memory Considerations​

Each parallel verifier uses additional memory:

  • Stack: 16 MB per thread (-Xss16m JVM setting)
  • Heap: Shared 2 GB pool (-Xmx2048m JVM setting)

With --cores 8, expect approximately 128 MB of stack memory plus shared heap usage. For very high core counts, monitor memory to avoid contention.

Combining with Other Flags​

With timeout​

Parallelism can reduce wall-clock time, allowing shorter timeouts:

sector9 --verify --cores 4 --verify-timeout-ms 30000 file.sr9

With JSON output​

For CI integration with parallel verification:

sector9 --verify --cores 4 --json file.sr9

With counterexamples​

Debug verification with parallelism and model extraction:

sector9 --verify --cores 4 --counterexample file.sr9

Environment Variable Override​

The SILICON_FLAGS environment variable can pass additional flags directly to Silicon:

SILICON_FLAGS="--numberOfParallelVerifiers=4" sector9 --verify file.sr9

Use this only for advanced Silicon tuning. It is passed through to the backend and can conflict with --cores if you duplicate the same Silicon option.

For raw emitted VPR files:

VERIFY_VPR_PARALLEL_VERIFIERS=2 ./scripts/verify-vpr.sh debug.vpr

Prefer the default one-worker setting for performance baselines, then run file-level jobs in parallel outside Silicon when comparing several generated VPR files.

Troubleshooting​

Verification is not faster with more cores​

  • Check method count: Single-method programs do not benefit from parallelism
  • Profile quantifiers: Complex quantifiers are SMT-bound, not parallelizable
  • Reduce nesting: Deeply nested quantifiers serialize on the solver

High memory usage​

  • Reduce cores: Each thread adds memory overhead
  • Use bounded quantification: Unbounded quantifiers increase solver state

Inconsistent results​

  • Use --deterministic: Ensure reproducible verification artifacts
  • Reduce parallelism: Lower core counts have less scheduling variance
  • Compare with --cores 1: This isolates backend scheduling from proof changes

Implementation Details​

The verification pipeline:

  1. Sector9 translates Sector9 source to Viper intermediate representation
  2. Silicon is launched as a Java subprocess with --numberOfParallelVerifiers
  3. Silicon spawns worker threads that consume proof obligations
  4. Z3 solves SMT queries from all threads
  5. Results are collected and mapped back to source locations

Process isolation:

  • Silicon runs in its own session group (setsid)
  • Timeout termination sends SIGTERM then SIGKILL to the entire process tree
  • This ensures Z3 child processes are properly cleaned up

Summary​

  • --cores N sets parallel verification threads (mapped to N-1 Silicon verifiers)
  • Default is single-threaded verification
  • Best for programs with multiple independent methods
  • Memory scales with core count (16 MB stack per thread)
  • Combine with --verify-timeout-ms for faster CI pipelines
  • Use SILICON_FLAGS for advanced Silicon configuration
  • Prefer --verify-timeout-ms and --deterministic in CI