X hits on this document

Powerpoint document

Algorithmic Verification of Concurrent Programs - page 11 / 100

218 views

0 shares

0 downloads

0 comments

11 / 100

Abstractions: an example

requires m == UNLOCK

void compute(int n) {

   for (int i = 0; i < n; i++) {

       assert m == UNLOCK;

       m = LOCK;

       while (x != y) {

           assert m == LOCK;

           m = UNLOCK;

           Sleep(1);

           assert m == UNLOCK;

           m = LOCK;

       }

       y = f (x);

       assert m == LOCK;

       m = UNLOCK;

   }

}

requires m == UNLOCK

void compute( ) {

   for ( ; * ; ) {

       assert m == UNLOCK;

       m = LOCK;

       while (*) {

           assert m == LOCK;

           m = UNLOCK;

           assert m == UNLOCK;

           m = LOCK;

       }

       assert m == LOCK;

       m = UNLOCK;

   }

}

Document info
Document views218
Page views218
Page last viewedSat Dec 03 00:23:37 UTC 2016
Pages100
Paragraphs1586
Words3927

Comments