The RPC-Memory Specification Problem: Problem Statement

I don’t remember how this came about, but Manfred Broy and I organized a Dagstuhl workshop on the specification and verification of concurrent systems. (I’m sure I agreed to this knowing that Broy and his associates would do all the real organizing.) We decided to pose a problem that all participants were expected to solve. This is the problem statement.

There is an interesting footnote to this workshop. As explained in the discussion of [50], I don’t believe in writing specifications as a conjunction of the properties that the system should satisfy. Several participants used this approach. I thought that the high-level specification was sufficiently trivial that by now, people would be able to specify it in this way. However, Reino Kurki-Suonio noticed an error that was present in all the “purely axiomatic” specifications–that is, ones that mentioned only the interface, without introducing internal variables.