X hits on this document

Powerpoint document

Algorithmic Verification of Concurrent Programs - page 17 / 100

358 views

0 shares

0 downloads

0 comments

17 / 100

int t;

L0: acquire(l);

L1: t := x;

L2: t := t + 1;

L3: x := t;

L4: release(l);

L5:

pre  x = 0;

post  x = 2;

int t;

M0: acquire(l);

M1: t := x;

M2: t := t + 1;

M3: x := t;

M4: release(l);

M5:

A

B

B@M0x=0,B@M5

B@M0x=0,B@M5



B@M0x=0,B@M5



B@M0x=0,B@M5



B@M0x=1,B@M5



B@M0x=1,B@M5

A@L0x=0,@L5

A@L0x=0,@L5



A@L0x=0,@L5



A@L0x=0,@L5



A@L0x=1,@L5



A@L0x=1,@L5

Document info
Document views358
Page views358
Page last viewedSun Jan 22 01:44:48 UTC 2017
Pages100
Paragraphs1586
Words3927

Comments