Determining System State

Defined by:
-A set of processes
-A set of channels connecting these processes

A series of actions or steps taken to achieve an end

Defined by:
-An initial state
-A sequence of events that happen during the process

An actions that may change a variety of things:
-State of the process
-State of an adjacent channel

Defined by:
-Process p in which it occurs
-State s of p immediately before the event
-State s' of p immediately after e
-Channel c whole state gets altered by the event (if it is)
-Message m that is sent or received along c (if it is)

Unidirectional communication that connects two processes

Assumed to be error free, with an arbitrary delay

Defined by:
-The sequence of messages sent from one end but not received by the other, calculated by n-m

(n = messages sent by sending process)
(m = messages received by receiving process)

Defined by:
-A meaningful collection of the states of each process and channel in the distributed system D
(Meaningful means a message must be in just one state, and not missing)

Creates a consistent and stable record of global states at a certain time.

Doesn't interfere with the underlying computation nor require the use of a common clock/perfect synchronisation.

Some problems can be solved if the global state can be determined.

For this, we need a stable state, determined by Boolean function Y(S), where:
-Y = predicate function
-S = global state

Once this is true, all global states reachable from S are true

Sends out a message to an initial process to send out a marker.

Marker sending rule for any process:
-Record state of process
-For each channel c it points towards, send a marker along c before sending any new messages

Marker receiving rule for any process:
-Upon receiving the marker, if there is no recorded state, record the state, execute send rule, and record state of c as an empty sequence
-If there is a recorded state, record the state of c as the sequence of messages received after recording until now

Sometimes the final snapshot produces may not be the same as the one that actually occurred, at least in the sequences it stores. It will, however, lead to the same result.

To get the same sequence, we mark each event as either a prerecording event or a postrecording event, and interchange prerecording events with the previous postrecording event.

Even without this, we can still get the stable state, as the same results are achieved.