True Concurrency and Atomicity. A model checking approach with contextual Petri nets

      Аннотация: Concurrent software is notoriously error-prone due to the possible unexpected interactions between concurrently executing processes. Testing is often not effective in discovering such errors since such intereferences heavily depends on the chosen scheduling and can appear very rarely. In the book we propose an approach for statically proving the absence of undesired interferences in concurrent programs. The approach is based on the definition of a so-called true concurrent semantics of the program which explicitly describes the possibly concurrent computation steps and their mutual dependencies. In the analysis we focus on atomicity properties, which assert that a program block acts in any computation as it were executed in isolation.

Ключевые слова: Concurrency, Contextual, Model checking, Multithreading, petri net thread