X hits on this document

Powerpoint document

Algorithmic Verification of Concurrent Programs - page 10 / 100

286 views

0 shares

0 downloads

0 comments

10 / 100

Abstractions: an example

requires m == UNLOCK

void compute(int n) {

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

       Acquire(m);

       while (x != y) {

           Release(m);

           Sleep(1);

           Acquire(m);

       }

       y = f (x);

       Release(m);

   }

}

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;

   }

}

Document info
Document views286
Page views286
Page last viewedSat Dec 10 01:51:39 UTC 2016
Pages100
Paragraphs1586
Words3927

Comments