| 
|
Quote: for proofs, can treat a sequence as atomic if it consists of right movers (V) followed by left movers (P)
topics >
all references >
references i-l >
Topic:
proving concurrent programs
Topic:
critical regions
Quotation Skeleton
D-reductions can now be defined. Definition. Replacing S_1; … ;S_n [with the same, uninterruptible sequence] is a D-reduction provided [it consists of right movers followed by left movers and, except for S_1, each S_i can always execute]. … In general, D-reduction then preserves any property that … [e.g., halting] Google-1 Google-2
Copyright clearance needed for quotation.
Topic: proving concurrent programs (37 items)
Topic: critical regions (58 items)