xcfa

Overview

Note that a textual representation is currently not in development. Use the XCFA Builder API for constructing XCFAs.

This project contains the eXtended Control Flow Automata (XCFA) formalism. Its main purpose is to describe programs as groups of graphs, where edges are annotated with program statements and each graph represents a single procedure in a single process. The project contains:

• Classes to represent XCFAs.
• A domain specific language (DSL) to parse XCFAs from a textual representation.
• A program transformation method that takes LLVM IR and creates an XCFA.

Every XCFA model consists of global variables and XcfaProcess definitions. XcfaProcesses consist of thread-local variables and XcfaProcedure definitions. XcfaProcedures are akin to the CFA models, in the sense that they consist of local variables, XcfaLocations and XcfaEdges; and XcfaEdges contain zero or more XcfaLabels.

Semantically, the XCFA formalism describes an asynchronous system, where processes are constantly executing statements on enabled transitions nondeterministically, until no such process remains (which either means a deadlock situation, or a completed execution). Statements are always atomic, but groups of statements can also be specified to be atomic when enclosed among AtomicBeginStmt and AtomicEndStmt statements. After any number of executed AtomicBeginStmts a single AtomicEndStmt ends the atomic block, and an AtomicEndStmt is no-op without a preceding AtomicBeginStmt.

XCFA models can be static or dynamic depending on whether all threads are spawned on entry, or threads can spawn and await other threads.

XcfaLabels

XcfaLabels are used in place of the CFA-like statements. The change was warranted by the excessive use of meta-statements (i.e., statements that do not modify the actual data state but rather contain metainformation on the program flow).

The following labels are used:

• AtomicBeginXcfaLabel: signals the beginning of an atomic (uninterruptible) block
• AtomicEndXcfaLabel: signals the end of an atomic block
• ProcedureCallXcfaLabel : invokes a procedure with a set of in/out/inout parameter expressions.
• StartThreadXcfaLabel: spawns a new process from an XcfaProcess template with a set of parameter expressions
• JoinThreadXcfaLabel: join a running process based on its unique PID (i.e., await its termination)
• LoadXcfaLabel: Loads a global variable into a local variable. Semantics are tie to the governing memory model. An additional label (ordering) can be given to the label, which can be referenced by the memory models.
• StoreXcfaLabel: Stores a local variable into a global variable. The same notes apply to this label as to the LoadXcfaLabel.
• FenceXcfaLabel: Signals a synchronization among global memory operations. The same notes apply to this label as to the LoadXcfaLabel.
• SequenceLabel: Grouping a sequence of labels into a single unit. See SequenceStmt for its motivation.
• NondetLabel: Grouping nondeterministic alternatives together. See NondetStmt for its motivation. Support for this lable is experimental.
• StmtXcfaLabel: Contains a single Stmt.

Related projects

• cfa: The ancestor project of the XCFA formalism, it can represent single-process single-procedure programs.
• xcfa-cli: An executable tool (command line) for running analyses on XCFAs.
• xcfa-analysis: The analyses that work on XCFAs.
• cat: The memory modeling language that is used by the analyses above.
• c-frontend: The c-frontend