Computing platforms with many CPUs and/or CPU cores are omnipresent nowadays. This holds even for embedded systems. In order to fully benefit from such architectures, concurrent programming is necessary. However, programming concurrent applications is significantly harder than producing sequential code since one additionally needs to properly synchronise all the concurrently running tasks. Improper synchronisation often leads to errors (such as data races, deadlocks, atomicity violations, order violations, etc.) that can have disastrous consequences but that are extremely difficult to detect. The reason is that such errors can manifest extremely rarely, and it is thus very difficult to catch them by traditional testing.

At the same time, concurrency is a very significant obstacle for current analysis and verification methods too. Methods of lightweight static analysis often suffer from quite significant imprecision on concurrent code despite a lot of effort has been invested and is still being invested into their improvement in this area. Model checking can in theory provide a guarantee that all such errors will be discovered in a precise way, but it suffers from scalability issues on large systems, and it may also have problems with various features of real-life code (user inputs, network communication, dealing with file systems and databases, etc.). Various forms of bounded model checking or systematic testing of concurrent code [DAC1, DAC2] improve the scalability but still suffer from similar issues.

An alternative to the above approaches is dynamic analysis (performed at runtime during testing runs or even during production runs) that not only monitors the activity of the system under test but tries to extrapolate the behaviour seen in the testing runs and to produce warnings about possible errors in the system even though such errors have not been witnessed in the performed runs. Various specialised checkers, e.g., [DAC5, DAC6, DAC7, DAC8, DAC9, DAC10], capable to produce such warnings have been developed for different kinds of concurrency errors, such as data races, deadlocks, atomicity violations, or breakage of so-called contracts for concurrency, which can encode numerous more specific kinds of concurrency errors (atomicity violation, order violation, etc.).

These approaches cannot guarantee overall soundness: they can at most guarantee soundness wrt the witnessed testing runs – this is, they can guarantee that if symptoms of an error appear in these runs, a warning will be produced. On the other hand, they can be more scalable and can cope better with various features of real-life code than model checking and can avoid various sources of false alarms that are problematic for static analysis (such as which memory objects are available to which threads at which moment).

Moreover, the effectiveness of extrapolating dynamic analyses can be further improved by combining them with so-called noise injection methods [DAC3, DAC4]. Such methods try to disturb the scheduling of concurrently executing threads (e.g., by injecting context switches, delays, etc. into the execution) such that thread interleavings that are otherwise rare manifest more often. (Note that the produced interleavings are still valid – unless real-time features are in play.) With noise injection, one can sometimes even use precise checkers (i.e., without any extrapolation and hence with no false alarms) and still can catch very rare behaviours even in industrial applications [DAC11].