X hits on this document

Powerpoint document

Algorithmic Verification of Concurrent Programs - page 69 / 100

290 views

0 shares

0 downloads

0 comments

69 / 100

Context-bounded reachability (I)

for each thread t {

   ComputeRTClosure(t)

}

for each (s 









> 0) {

’’

’



A work item (s, p) indicates that from state s,

p(i) contexts of thread i remain to be explored

ComputeRTClosure(u) {

   …



       Remove (s, s’) from F

       for each u-successor s’’ of s’

           add (s, s’’) to F

       Add (s, s’) to RT(u)

   }

}

Document info
Document views290
Page views290
Page last viewedSat Dec 10 18:59:29 UTC 2016
Pages100
Paragraphs1586
Words3927

Comments