摘要:All commercially available processors (even the processors used in mobile devices) have the typical multicorearchitecture (Yeap, 2013) – the shared memory programming model dominated over the sequential programmingmodel as the optimal way for obtaining maximum performance offered by these architectures. Execution orderassumptions between instructions and atomicity when accessing legacy variables from the sequentialprogramming model are no longer valid in the new model, whose implicit non-determinism when runningconcurrent programs forces programmers to use some synchronization mechanism to make sure these propertiesare present. Frequently, programmers make mistakes when synchronizing the processes, which results in newprogramming errors such as deadlocks, race conditions, order violations, simple atomicity violations, andmultivariable atomicity violations. These errors cannot be detected by traditional debugging methods, so toolsthat can help detecting and correcting them are required.