For my google summer of code project, I worked on implementing parallel block analysis for CPAchecker. Basing the project on the existing infer project, my work this summer had the following main goals: - Parallel Decomposition of the CFA - Establish a communication method between worker nodes and the root - Implement formula strengthening for predicate CPAs between worker nodes

We accomplished this by breaking up the original CFA into multiple “blocks” which currently each represent a single reachable function in the program. Each block has all of its outgoing “function call edges” removed such that any analysis done on the block will over-approximate said function. Working with the existing precision, the block finishes its analysis with by producing a list of “ErrorCondition” or “PostCondition” states which represents violation states reached and the final state of the block respectively.

When independent block analysis conclude, they broadcast their messages to all the workers that are callers of that block. The callers use the data in the ErrorCondition and PostCondition formulas to “strengthen” their next analysis specifically on the precision of the function call edge that was previously over-approximated. This process continues until all strengthening messages have been sent. If the main function’s final analysis includes an “ErrorCondition” message, then we have found a violation. Otherwise we have a proof.

Completed Work

My work was done in the following branch - infer-using-dcpas

As there is still more work that we want to add to this branch, it hasn’t been merged yet. However, it includes all the worked described above.

We ran into some interesting corner cases while benchmarking that are still being addressed before we can get proper results. Specifically variable collisions in strengthening formulas that will occur when verifying programs like the following:

int grandom(){
  return __VERIFIER_nondet_int();
}

int foo(){
  return grandom();
}

int bar(){
  return grandom();
}

int main() {

  int x = foo();
  int y = bar();
  if (!(y == x)) {
    ERROR: {reach_error();abort();}
  }

  return 0;
}

Evaluation

We are currently waiting on getting a few of the unforeseen variable collision bugs worked out before we can get a proper evaluation written up.

Future Work

gRPC

The framework put together for parallel block analysis has lots of opportunity for future projects and improvement! Currently we are working on switching out our actor-based model with a proper gRPC protocol for distributing parallel work. This should lead to significant performance gains as our parallel architecture will actually be able to distribute across multiple machines.

Configuration Options

Additionally, we plan to add configurations options that give users more control over precision and granularity of their analysis. Some examples of this would be limiting the number of strengthens per block or how many functions to include inside each block.

Incremental Evaluation

Since our block graph is currently modeled like a DAG, it is possible to store results from previous builds and only run analysis on blocks that were edited as well as its dependees. This could make parallel block analysis a great candidate for CI/CD pipelines.