The supercompiler SCP 4 verification. Alexei P. Lisitsa The University of Liverpool. Andrei P. Nemytykh Program System Institute, Russian Academy of Sciences. - презентация

1 The supercompiler SCP 4 verification. Alexei P. Lisitsa The University of Liverpool. Andrei P. Nemytykh Program System Institute, Russian Academy of Sciences.

2 Verification of parameterized systems by the supercompiler SCP4. ( ) Successful experiments on verification of global cache coherence protocols: –IEEE Futurebus+, MOESI, MESI, MSI, The University of Illinois, DEC Firefly, Berkeley, Xerox PARC Dragon. More global parameterized protocols: –Java Meta-Locking Algorithm, Reader-Writer protocol.

3 A class of parameterized cache coherence protocols. Cache coherence protocols are used to maintain data consistency in multiprocessors systems equipped with local fast caches (elements of memory). A class of such protocols can be described as the following games: Let n baskets be given. The i-th basket contains x i stones. A step of a game is a permutation of y ik stones from the i-th basket to the k-th basket (for all 0 < i,k < n+1), if the y ik satisfy some conditions. If two or more steps can be done in the same time, then a random choice from the steps takes place. Let a start configuration of such a game be given, then the data consistency problem is a non-reachability problem of some configurations in the game.

4 Testing. Given a total recursive function f: D M, let Im(f) be a subset of the truths set of a total recursive recursive predicate. Let P be a program implementing ; P f be a program, such that d 0 D the call P f (d 0 ) terminates. Let P f be assumed to implement f. Testing of P f with respect to a post-condition is a program T: D {True, False} implementing the following composition P P f. d 0 D the result of evaluation of T(d 0 ) = True confirms correctness of P f on d 0, while T(d 0 ) = False gives a test d 0 where P f is invalid.

5 Verification. Running over the whole D with the valid result of the testing verifies P f with respect to the post-condition. Let be an optimizer such that the result of ( P P f,d) is a program with a simple syntactical property guarantying that Im( ) = {True}. Let the result of optimization, by definition of, implements an extension of the partial function implemented by the program to be transformed (in our case P P f ). In such a case we have verification of P f with respect to the post- condition.

6 Encoding of a class of cache coherence protocols. Evolution of the set of states of a multiprocessor system is a non-deterministic dynamic system with discrete time. Let Int(time,InitConfig) be an interpreter of the system, such that given a start configuration InitConfig of the system Int returns the configuration Config the system reaches in time. To simulate the non-deterministic choice we mark the times tacts with the random actions taking place in the system. The correctness of the protocols is expressed by unreachability of a special kind of the configurations and it is tested by a predicate-program (Config). The task for a supercompiler is: specialize the following composition Int(time,InitConfig 0 )

7 The MOESI protocol. (The proof by SCP4: induction on time) Theorem 1 Theorem 2 True2 Lemma $# # # $ $ $$$ True

8 Verification of the Xerox PARC Dragon cache coherence protocol. An error in a description of the protocol has been found as a result of analyzing of the residual program: –G. Delzanno, Automatic Verification of Parameterized Cache Coherence Protocols. and a test indicating the error was constructed. Successful verification of a corrected version of the description of the protocol was done: –

9 Languages dependence. (The MOESI protocol) RandomAction { … … = (invalid e.x1) (modified ) (shared I e.x3 e.x4) (exclusive )(owned e.x2 e.x5); … } Append { () (e.y) = e.y; (s.z e.x) (e.y) = s.z ; } RandomAction { … … = (invalid e.x1) (modified ) (shared I ) (exclusive )(owned ); … }

10 References [1] Lisitsa A. P., and Nemytykh A.P., Verification of parameterized systems using supercompilation. In Proc. of the APPSEM05, Fraunchiemsee, Germany, September [2] Lisitsa A. P., and Nemytykh A.P., Towards verification via supercompilation. In Proc. of the COMPSAC2005, [3] Lisitsa A.P., and Nemytykh A.P., Verification as parameterized testing (Experiments with the supercompiler SCP4). (In Russian), Submitted to the journal Programming, [4] Lisitsa A. P., and Nemytykh A.P., Work on errors. (In Russian), Submitted to the conference Program Systems: Theory and Applications, 2006.

11 Thank you!