On the verification of concurrent programs under weak consistency and persistency
Concurrent programs are running over data storage infrastructures that in general do not guarantee strong consistency (where every update of the data storage structures is visible to all processes). The consistency model defines the possible orders in which different processes can see updates issued by the program. These orders do not coincide with the interleaving of behaviors executed in program order. This makes unintuitive and very complex reasoning about program behaviors under weakly consistent models. In addition, some of the infrastructures include a mechanism for making data persistent so that executions can be resumed upon crashes from persistent states. Again, the order in which data in the (volatile) memory is persisted does not necessarily coincide with the program order. The persistency model defines the possible persistent states that are observable when crashes happen. The combination of both aspects (visibility of updates and their persistency) makes the verification of concurrent programs quite challenging. We provide in this talk a high level presentation of these aspects and of the issue of verifying programs in this context.
The talk is based on a joint work with Parosh Abdulla, Mohamed Faouzi Atig, Narayan Kumar, and Prakash Saivasan.