Lecture Notes for Concurrent Programming

10 June 2003 - Atomicity and Synchronization

Outline

• Conditional synchronization.

  • Producer and consumers.

  • The await statement.

  • The co statement rule.

• Sequential statement atomicity

  • sequential statement non-atomicity.

  • Atomic statements.

  • Critical references.

  • The At-Most-Once property.

Producer and Consumer

• Consider

  data buffer
  
  process producer       process consumer 
    while true	         while true     
      buffer = p()           c(buffer)    
  

• Invariant: all data produced by p() is consumed by c().

  • Almost; don't forget the buffer.

  • Inv: dseq_p = dseq_c or
dseq_p = dseq_c + buffer

• The invariant is initially true: dseq_p = dseq_c = empty.

• Neither process preserves the invariant.

  • producer can overwrite data in the buffer.

  • consumer can re-read old data in the buffer.

• These problems cannot be solved with mutual exclusion.

Produce-Consumer Synchronization

• The original producer-consumer ignored the buffer state.

  • buffer is either ready to read (full) or ready to write (empty).

  data buffer
  bool empty = true
  
  process producer         process consumer
    while true		   while true
      while !empty skip	     while empty skip
      { empty }		     { !empty }
      buffer = p()	     c(buffer)
      empty = false;	     empty = true
  

• Now only empty buffers get written and full buffers get read.

  • The preconditions to the p() and c() statements see to that.

Conditional Synchronization

• Conditional synchronization delays a thread's execution until some condition is true.

  • The condition is specified by a state predicate.

  • There's no a priori requirement that the condition ever be true.

• Conditional synchronization can't be provided by mutual exclusion.

  • Mutual exclusion conflicts with conditional synchronization.

• Spinning on the predicate in a while statement is one way to provide conditional synchronization.

  while empty skip
  { !empty }
  c(buffer)
  

  • It's not a good use of hardware resources, though.

  • The predicate may have atomicity problems too.

The await Statement

• There's many different ways of providing conditional synchronization.

  • The best way is context dependent.

• Abstract away the different implementations in a conditional-synchronization statement.

• The statement await B blocks the executing thread until B is true.

  • There's no requirement that B eventually be true.

• The await statement is generally too expensive to implement.

  • There are special-case uses of the await statement that are efficient to implement.

await and Atomicity

• Given await B ; S , B may be interfered with after falling out of await B.

  • B must reference at least one write-set variable.

• Our ol' pal atomicity helps us here.

• If the triple

  { P and B }  S  { Q }
  

  holds, then the Await Rule lets us conclude that the triple

  { P }  < await B ; S >  { Q }
  

  holds too.

  • { P and B } can't be interfered with in
    < await B { P and B } S >.

  • { P } can be interfered with, though.

• < await B ; S > is not executed until B is true.

  • Blocking inside an atomic sequence is a bad idea.

• But you have to implement both atomicity and the await statement.

The co Statement Rule

• If { Pi } Si { Qi } hold for 1 <= i <= n and are interference free then the co Statement Rule

  { P1 and P2 and ... and Pn }
  co S1 || S2 || ... || Sn oc
  { Q1 and Q2 and ... and Qn }
  

  holds too.

• The co-statement precondition is the precondition for each Si in the co statement.

  • You can use and elimination to get back the original precondition.

• The combination of the individual statement postconditions gives the co-statement postcondition.

Sequential Statement Atomicity

• We've assumed that sequential statements execute atomically.

  • A statement executing atomically executes alone.

• This is a pleasant and useful assumption.

  • It cuts down on the number of possible execution histories under concurrency.

  • It also simplifies and makes obvious the remaining histories.

• For example, Under the atomicity assumption

  co x = x + 1 || x = x + 1 oc
  

  is equivalent to

  co < x = x + 1 > || < x = x + 1 > oc
  

  and the latter co statement has only two equivalent sequential executions:

  1. x1 = x1 + 1 ; x2 = x2 + 1 or

  2. x2 = x2 + 1 ; x1 = x1 + 1

Sequential Statement Non-Atomicity

• Sequential statements are rarely - if ever - atomic.

  C++	x86 assembly	pseudo-code
  x = x + 1	movl %esp, %ebp subl $4, %esp leal -4(%ebp), %eax incl (%eax)	move r0 x add r0 1 move x r0

• The possible concurrent executions of non-atomic statements are more numerous and obscure than with atomic statements.

  • Assuming the four-statement x86 sequence above, the statement

    co x = x + 1 || x = x + 1 oc
    

    has (2*4)!/4!² = 40320/576 = 70 possible sequential executions.

  • Many of the 70 possible sequential executions produce results at odds with expected sequential behavior.

    move r1 x move r2 x add r1 1 add r2 1 move x r1 move x r2

    This is assembly language sequence equivalent to executing x = x + 1

Atomic Statements

• Treating statements at the assembly level isn't a good idea.

  • There's too much detail to manage.

  • Sensitive to changes on hardware and software.

  • Some assembly-language instructions aren't atomic either.

• Putting atomicity brackets <> around each statement isn't a good idea.

  • It's difficult to implement and expensive to use.

• We want the effect of atomic execution without the cost of atomic execution.

• Reguardez: S appears to be atomic if it accesses only read-set shared variables.

  • No shared variables change while S executes.

  • Unfortunately, accessing only read-set shared variables is restrictive.

Critical References

• Consider co x = y + 1 || y = z + 1 oc .

  • A critical reference is a reading reference to a write-set shared variable.

  • x = y + 1 either reads the old or new value of y.

  • Executing

    co x = y + 1 || y = z + 1 oc
    

    is equivalent to executing

    co < x = y + 1 > || < y = z + 1 > oc
    

• Consider co x = y + y || y = z + 1 oc .

  • x = y + y has two critical references.

  • x = y + y can read both the old and new values of y.

  • This has no equivalent atomic-statement execution.

• Remember co x = x + 1 || x = x + 1 oc ?

  • x = x + 1 has one critical reference to x, but it also modifies the read-set variable x.

  • There's no equivalent atomic execution for this.

The At-Most-Once Property

• The statement S obeys the At-Most-Once property if

  1. S contains at most one critical reference and doesn't modify a read-set shared variable, or

  2. S contains no critical references.

  In the second case, S may write a read-set variable.

• A statement obeying the At-Most-Once property executes as if it were atomic.

Data Atomicity

• Operations on large, multi-word data types are rarely atomic.

  C++ code	Sparc assembly
  std::pair<int, int> i, j; i = j;	ld [%fp-32], %o0 st %o0, [%fp-24] ld [%fp-28], %o0 st %o0, [%fp-20]

• Non-atomic data violates the At-Most-Once property.

  • The statement

    co buffer = p() || c(buffer) oc
    

    may not be equivalent to either of the sequential executions

    buffer = p() ; c(buffer)
    

    or

    c(buffer) ; buffer = p() 
    

Points to Remember

• Mutual exclusion and conditional synchronization are the two major forms of concurrency control.

  • They are not interchangeable.

• The await statement produces conditional synchronization.

  • It's a design tool; it needs to be implemented.

• Sequential statements are usually not atomic.

  • This causes problems under concurrency.

• Sequential statements obeying the At-Most-Once property are effectively atomic.

This page last modified on 12 June 2003.