Memory modeling in PVS
Nowadays, a lot of software is designed to be executed on different
processors simultaneously. Different threads are working on the same
problem, and operate on the same memory location at the same time.
Consequently, synchronization is required. A new algorithm to deal with
the situation has been proposed. This method has some severe advantages
compared with a traditional solution.
In this lecture, we will discuss a PVS specification of this problem, and
prove the functional equivalence between the two solutions, while the new
algorithm exposes its benefits. We will also compare the PVS specification
with a VDM specification, and discuss some differences.