Chapter 2: Abstractions

interleaving

process or methodology to make a system more efficient, fast, and reliable by arranging data in a noncontiguous manner

when we have multiple processes running, have to account for all the different possible ways

the scheduler can interrupt 1 process and pick up a 2nd process when it chooses

state transition diagram

what you put in these states are:
the statements that are going to be executed next
the variables and their current values

when a particular process goes, assume what the code that was up executes

atomic statement

statement cannot be interleaved at a lower level of abstraction

computation

directed path through a graph (state-transition diagram) starting from the initial state and ending in a halt state

scenario

table representation of a computation

concurrency analysis

- specify which statements are atomic
- assume arbitrary interleaving of atomic statements
- is the algorithm correct for all interleavings?

safety property

"always"

P must be true in every state in every computation

usually rules out bad behavior

liveness property

"eventually"

in every computation, there is some state in which P is
true

ensures the system does what it is supposed to do

duality

if P is a safety property, then ¬P is a liveness property
¬(∀x R : P) ≡ (∃x R : ¬P)

if P is a liveness property, then ¬P is a safety property
¬(∃x R : P) ≡ (∀x R : ¬P)

weakly fair

a scenario is weakly fair if, at any state in the scenario, a statement that is continually enabled, eventually appears in the scenario

if a statement is capable of running in a weakly fair scenario, it will eventually run

weak fairness

fairness depends on the scheduling policy of the
operating system

critical reference

variable v is a critical reference if:
(a) it is assigned in one process and has an occurrence
in another process, or
(b) it occurs in an expression in one process and is
assigned in another

limited critical reference (LCR)

program satisfies LCR if each statement contains at
most 1 critical reference

if an algorithm satisfies LCR, then it behaves the same
regardless of whether its statements are atomic (do not need to modify your algorithm with temp to mimic the lower level)

volatile variable

specifying a variable as volatile instructs the compiler to load and store the value of the variable at each use,
rather than to optimize away these loads and stores.

thread

programs during execution that is under the control of a process

threads vs processes

during execution that is under the control of ..
- thread: a process
- process: an operating system

communicate..
- thread: via shared memory
- process: via message passing