X hits on this document

Powerpoint document

Algorithmic Verification of Concurrent Programs - page 95 / 100

265 views

0 shares

0 downloads

0 comments

95 / 100

Happens-before graph

T1:            T1:       T1:                                               T1:           T1:        T1:

acq(m)      x:=1      rel(m)                                          acq(n)      y:=1      rel(n)

T2:            T2:       T2:

acq(m)      x:=2      rel(m)

An execution is a total order over thread actions

Thehappens-before graph of an execution is a partial order over thread actions

Alllinearizationsofahappensbeforegraphareexecutionsandgeneratethesamefinalstate

Thehappensbeforegraphisacanonicalrepresentativeofanexecution

Document info
Document views265
Page views265
Page last viewedThu Dec 08 02:55:14 UTC 2016
Pages100
Paragraphs1586
Words3927

Comments