THREADS AND LOCKS

Rules for Volatile Variables

17.7

17.6   Rules about the Interaction of Locks and Variables

Let

T

 be any thread, let

V

 be any variable, and let

L

 be any lock. There are certain

constraints on the actions performed by

T

 with respect to

V

 and

L

:

Between an

assign

 action by

T

 on

V

 and a subsequent

unlock

 action by

T

 on

L

,

a

store

 action by

T

 on

V

 must intervene; moreover, the

write

 action corre 

sponding to that

store

 must precede the

unlock

 action, as seen by main mem 

ory. (Less formally: if a thread is to perform an

unlock

 action on

any

 lock, it

must first copy

all

 assigned values in its working memory back out to main

memory.)

Between a

lock

 action by

T

 on

L

 and a subsequent

use

 or

store

 action by

T

 on

a variable

V

, an

assign

 or

load

 action on

V

 must intervene; moreover, if it is a

load

 action, then the

read

 action corresponding to that

load

 must follow the

lock

 action, as seen by main memory. (Less formally: a

lock

 action acts as if it

flushes

all

 variables from the thread's working memory; before use they must

be assigned or loaded from main memory.)

17.7   Rules for Volatile Variables

If a variable is declared

volatile

, then additional constraints apply to the actions

of each thread. Let

T

 be a thread and let

V

 and

W

 be volatile variables.

An

use

 action by

T

 on

V

 is permitted only if the previous action by

T

 on

V

 was

load

, and a

load

 action by

T

 on

V

 is permitted only if the next action by

T

 on

V

is

use

. The

use

 action is said to be  associated  with the

read

 action that corre 

sponds to the

load

.

A

store

 action by

T

 on

V

 is permitted only if the previous action by

T

 on

V

 was

assign

, and an

assign

 action by

T

 on

V

 is permitted only if the next action by

T

on

V

 is

store

. The

assign

 action is said to be  associated  with the

write

 action

that corresponds to the

store

.

Let action

A

 be a

use

 or

assign

 by thread

T

 on variable

V

, let action

F

 be the

load

 or

store

 associated with

A

, and let action

P

 be the

read

 or

write

 of

V

 that

corresponds to

F

. Similarly, let action

B

 be a

use

 or

assign

 by thread

T

 on

variable

W

, let action

G

 be the

load

 or

store

 associated with

B

, and let action

Q

be the

read

 or

write

 of

V

 that corresponds to

G

. If

A

 precedes

B

, then

P

 must

precede

Q

. (Less formally: actions on the master copies of volatile variables

on behalf of a thread are performed by the main memory in exactly the order

that the thread requested.)

407