Lecture Notes for Concurrent Programming

6 June 2002 - States and Properties

1. states

   1. a variable's state is a name-value pair

   2. a program's state is the state of all its variables

      1. not really all; usually globals, but not always

      2. may include hidden variables (the pc, status registers) and imaginary or ghost variables that do not appear in the program

   3. a state trace (or history) is a sequence of program states

      1. each state is one step away from the next

   4. states and state traces provide an important way to specify and think about program behavior

      1. focuses on the important part - the data's where it's at, after all

      2. abstract away much detail - what matters is where you end up, not how you get there

2. properties

   1. a property is a boolean statement about a program's state

      1. a property that is true is satisfied

   2. we'll use (quasi) predicate calculus to describe properties

   3. a property might be always true, or may eventually become true

      1. a safety property is an always true property

      2. a liveness property is an eventually true property

   4. a program can be characterized by a set of properties describing input and output behaviors

   5. given a program specified by properties

      1. the program satisfies its properties if any execution of the program leaves the properties satisfied

3. axiomatic semantics

   1. does a particular program satisfy its properties

      1. debugging - there's too many traces to debug

         1. each trace is difficult to understand - interleaving

         2. the act of debugging changes the trace - stepping in the same stream twice

      2. operational - this, then this, then this; too many traces again

      3. reason about program properties - cuts down on the work

   2. axiomatic reasoning about properties

      1. examine statements' effect on properties - the hoar triple {pre} s {post}

      2. if pre is true and s executes, then post is true

      3. proof outlines interleave properties and statements

      4. the axioms establish how each statement effects preconditions

         1. sequencing - if {p} s {q} and {q} s {r}, then {p} s ; s {r}

         2. assignment - {p[x <- e]} x = e {p}

         3. if - one branch, or two

         4. while - the loop invariant

         5. consequence - strengthening and weakening

         6. await - like a one-branch if

      5. interference

         1. a property may contain a write critical reference - one is too many; critical property (or assertion)

         2. some other step may invalidate the property - interference

         3. need to show noninterference - {C and pre} s {C}

            1. need to show this for all other statement s - that's usually a lot, but much fewer than than execution traces

         4. properties within atomic actions may be ignored

      6. the co statement axiom

4. avoiding interference

   1. four techniques for avoiding interference

      1. disjoint variables

         1. no write critical reference, no interference

         2. usually indicates a design error - using a global when a local would do

         3. you probably need other techniques too

      2. weaken the property

         1. take into account the effects of other statements

         2. use sparingly - properties can become huge otherwise

      3. use global invariants

         1. properties that are always true, no matter which step executes

         2. involves global variables

         3. critical assertions are a conjunction of global invariants and properties over local variables and uniquely written globals

         4. this is an important technique for structuring and reasoning about concurrent programs - reasoning in isolation

      4. use synchronization

         1. properties within atomic actions are not critical

         2. hide properties within atomic actions - granularity

         3. delay the conflicting statement until the critical assertion is false or can be made true by executing the statement

This page last modified on 16 June 2002.