1

Shared Variables:

Lecture notes prepared by Ali Hazemi, please send your comments to: ajh1@cec.wustl.edu

Homework 1 is due on Wednesday 9/15/99... Homework 1

Reference: Andrews, G.R., Concurrent Programming: Principles and Practice,

Benjamin/Cummings Pub. Co., 1991. (ch. 2-6)

The Nature of Concurrency (ch. 2)

Terminology and notation

Clarification of terms:

Sequential program characteristics: We have one machine and one thread of execution.

This is the way programming started. The thread of execution is really associated

With the program-counter which is normally incrementing one by one and if we have

special constructs such as go-to, program-counter is adjusted accordingly.

Concurrent program characteristics: We have possibly more than one machine and

possibly more than one thread of control. Processes/Threads typically interact with

Each other via shared data.

Parallel program characteristics: Special case of concurrent programs intended for parallel machines. Parallel can be shared-memory parallel machines (multiple processors share memory) or distributed-memory (each processor has its own memory).

Distributed program characteristics: Network processing, each processor has its own

memory and we have no shared-memory.

Basic concepts needed to denote concurrency:

What does it take to build a concurrent program?

Assume we have a block-structured language (variables have lexical scope) with

variable declarations which may be local or global to a context.

so now we can organize our program.

How do we change state?

The program has to carry out some activity and that generally represents change in state.

The typical mechanism for representing a change in state of a program is a statement.

Most typically we have assignment to variables, which change values of variables.

How can we combine the statements to make a complete program?

One basic way of combining is sequential composition. Typically denoted by S1:S2

Where S1 and S2 are statements.

So far we have a sequential program, What else do we need to denote concurrent programs?

One the first models that was introduced was: Having multiple sequential programs that are Sharing data(variables). To describe two sequential programs being executed in parallel (whatever that means!) we use a parallel construct for example: co S1 || S2 oc

We now have a program which consists of two sequential programs that are combined

By the parallel operator || into a concurrent program. Now taking advantage of the fact

That we have a block-structured language, we will have the form:

begin declarations; Process-name1 :: code-body1; … end

Examples:

co i:= 1 to n à a[i] := 0 oc

n statements executed in parallel a[1] := 0, a[2] := 0, …, a[n] := 0

x := 0; y := 0

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

z := x + y

two statements executed in parallel (whatever parallel means!)

x : = 0; y := 0

XPlus :: x := x + 1

YPlus :: y := y +1

end

z := z + y

Give name to two assignments (processes)

Semantics:

What does a program like above example mean?

There are many possible interpretations. For example what happens if x appears on the

left hand-side of two statements in a parallel construct?

Notation is not enough, We need semantics of concurrent program. We can not deal with

Concurrency unless we address two fundamental questions about the system the program

Runs on. One has to do with atomicity and the other with fairness of our system.

Atomicity and fairness assumptions of our system can change the semantics of our program significantly.

Models:

How have people historically assigned semantic to programming languages?

Do these semantics lead to verification and proof of correctness?

Operational semantics model: Models of semantics where the model is given in terms of

an abstract machine. We explain what a language does (statements of the language mean)

by inventing an abstract machine and showing all the effects of the language on the state

of this machine. For example if the abstract machine has memory locations for variables

and a program counter, we can define the meaning of the statement x := x +1 as a set of

operations on this machine that is: 1. Read the value of x into the accumulator, 2. increment the value in the accumulator by one, 3. Take the value in the accumulator and

put it back in the same memory location. We explain what the statements do in terms of

how they change the state of our abstract machine. Operational semantic models are used

for building simulators for the language.

Denotational semantics model: Models of semantics where the model is given in terms of functional mapping. For every program P, we calculate a mapping that maps the program to a mathematical entity M. For example a set or a recursive function. Typical ly M can be

A function that maps input into output. If we are given a program P, we can apply this

Denotational semantic transformation and get a function M. Now if we give the input of

P to M, the function M will give us the output that P would have produced had it finished

Execution. This model is also used for building simulator for languages.

Axiomatic semantics model: Models of semantics that are base on logic. They are based

On axioms and inference rules that allow us to prove properties of programs. These models are used for verification of correctness of our programs.

Atomicity

How indivisible operations (actions) on a system are?

An operation is atomic if we can think of it as happening logically in an instance of time.

If two operations are atomic they can NOT happen at the same time. For a sequential program

Each action (statement execution) appears to be atomic because we only have one thread of

Execution and intermediate states are not visible.

Formal reasoning is carried out using a formal programming logic.

Hoare triple for structured programs.

{P} s {Q} is true if whenever s is started in a state satisfying P and s terminates , the resulting state satisfies Q.

for example: { x > 0} z := y + w { z = 3}

Skip axiom: {P} skip {P}

Assignment axiom: {P ^x_e} x := e {P}

For example: {true} x:= 5 {x = 5}

{(x > 0) ^x₃} x := 3 {x > 0}

{(y > 7) ^x₃} x := 3 {y > 7}

Consequence axiom: P’ Þ P, {P} s {Q}, Q Þ Q’ |- {P’} s {Q’}
Sequential composition: {P} s1 {Q}, {Q} s2 {R} |- {P} s1; s2 {R}
Alternative rule: P Ù Ø (B₁ Ú … Ú Bn) Þ Q, for 1 £ i £ n {P Ù B_i }s_i {Q}

| - {P} IF {Q}

Iterative rule: for 1 £ i £ {I Ù B_i} s_i{I}

| - {I} DO {I Ù Ø (B_{1 Ú}…Ú B_n)}