Module Goblint_lib.RaceAnalysis

Data race analysis (race).

Data race analysis with tries for offsets and type-based memory locations for open code.

Accesses are to memory locations (memos) which consist of a root and offset. Root can be:

  1. variable, if access is to known global variable or alloc-variable;
  2. type, if access is to unknown pointer.

Accesses are (now) collected to sets for each corresponding memo, after points-to sets are resolved, during postsolving.

Race checking is performed per-memo, except must additionally account for accesses to other memos (see diagram below):

  1. access to s.f can race with access to a prefix like s, which writes an entire struct at once;
  2. access to s.f can race with type-based access like (struct S).f;
  3. access to (struct S).f can race with type-based access to a suffix like (int).
  4. access to (struct T).s.f can race with type-based access like (struct S), which is a combination of the above.

These are accounted for lazily (unlike in the past).

Prefixes (a.k.a. inner distribution) are handled using a trie data structure enriched with lattice properties. Race checking starts at the root and passes accesses to ancestor nodes down to children.

Type suffixes (a.k.a. outer distribution) are handled by computing successive immediate type suffixes transitively and accessing corresponding offsets from corresponding root tries in the global invariant.

Type suffix prefixes (for the combination of the two) are handled by passing type suffix accesses down when traversing the prefix trie.

Race checking happens at each trie node with the above three access sets at hand using Access.group_may_race. All necessary combinations between the four classes are handled, but unnecessary repeated work is carefully avoided. E.g. accesses which are pairwise checked at some prefix are not re-checked pairwise at a node. Thus, races (with prefixes or type suffixes) are reported for most precise memos with actual accesses: at the longest prefix and longest type suffix.

Additionally, accesses between prefix and type suffix intersecting at a node are checked. These races are reported at the unique memo at the intersection of the prefix and the type suffix. This requires an implementation hack to still eagerly do outer distribution, but only of empty access sets. It ensures that corresponding trie nodes exist for traversal later.

Given C declarations:

struct S {
  int f;
};

struct T {
  struct S s;
};

struct T t;

Example structure of related memos for race checking:

     (int)   (S)     (T)
        \   /   \   /   \
          f       s       t
            \   /   \   /
              f       s
                \   /
                  f

where:

All same-node races:

All prefix races:

All type suffix races:

All type suffix prefix races:

All prefix-type suffix races:

module Spec : sig ... end

Data race analyzer without base --- this is the new standard