What is this application?

This application facilitates the testing of weak memory-related phenomena by running tests
described by an XCFA formalism and a test environment.

How does this work?

The XCFA formalism is parsed and an in-memory object is built representing it.
Thereafter, this
model is compiled into bytecode by a JIT compiler using VIXL as its backend, which is then
executed concurrently and execution results are displayed to the user.
It is important to use
actual compiled code rather than write an interpreter, as most concurrency issues arise when
executing instructions immediately after each other.
An interpreter would introduce too much
overhead.

What is an XCFA?

XCFA is the abbreviation of eXtended Control Flow Automaton, and a formalism which represents a
program via a mathematical automaton.
A normal CFA (Control Flow Automaton) is made up of labels
and edges: labels are locations in the program, and edges are transitions between these
locations.
An XCFA is more than this in two fundamental ways: it is a collection of CFAs that
reside inside procedures, and these procedures are collected into threads.
The
semantics of these elements correspond to those of the same elements in a programming language
such as C/C++ or Java.

What is weak memory?

Modern multicore processors (such as the one most likely in this device) employ such
optimizations while executing instructions that result in a different execution order than the
order of instructions in the binary.
As the memory access time represents a huge bottleneck, a
buffer is used which is writable in a faster manner, and it will get flushed to memory while the
processor goes on to execute other instructions.
In the case of weak memory, the only
barrier to this is a successive memory operation to the same address, or a fence
instruction.
Most of the times this kind of optimization goes unnoticed, but sometimes the
programmer has to interface with it - e.g.
when using a processor that has a href="http: //infocenter.arm.com/help/topic/com.arm.doc.uan0004a/UAN0004A_a9_read_read.pdf">known
fault.

I am interested.
Where can I learn more?

• Theta (XCFA): GitHub repository


• Faulty HW, correct SW: ACM-TECS
  paper

Page navigation:

• < Prev
• Next >