Memory modeling in PVS

Pieter Audenaert

ABSTRACT

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.