How do we represent a distributed system so that we can compare designs, and then prove something about how it behaves?
Software architectures organise a complex system as components, connectors and data; system architectures place the components. Recurring organisations are architectural styles, which differ in how they couple processes in space and time. Architectures model structure, not behaviour, and prove nothing. Process algebra fills that gap for concurrency: a few operators (+, ;, ∥), laws that serve as axioms for proofs, and transition rules that serve as a reference for implementation. When the rules obey the laws, the implementation inherits formal properties. Physical distribution is still left out.
The basic ontology of Ch. 1 (computational processes in a context of machine, resources, time and space) is our ground. Now we need a general way to represent distributed systems, independent of their heterogeneous nature. Four questions frame it:
Two answers follow: the classical view of software and system architectures, borrowed largely from Tanenbaum & van Steen [2017], for structure; process algebra for behaviour.
To manage their complexity, distributed systems should be properly organised, and organisation is mostly expressed in terms of software components. The ways to organise components are classified as software architectures. Their many instantiations, with components given an actual place in the system, are often called system architectures.
A component is a modular unit with well-defined interfaces, replaceable within its environment. Interfaces go both ways: they are both required and provided.
A connector is an abstraction mediating communication, coordination and cooperation among components: anything providing a mechanism for interaction among them.
Together they produce a huge range of configurations, classified as architectural styles. Fielding gives the precise vocabulary:
A software architecture is an abstraction of the run-time elements of a software system during some phase of its operation. A system may be composed of many levels of abstraction and many phases of operation, each with its own software architecture.
A software architecture is defined by a configuration of architectural elements (components, connectors, and data) constrained in their relationships in order to achieve a desired set of architectural properties.
Architectural elements [Fielding, 2000]
The architectural properties of a software architecture derive from the selection and arrangement of components, connectors and data. They include functional properties and quality attributes such as ease of evolution, reusability of components, efficiency and dynamic extensibility. Properties are induced by constraints, and architectural constraints are often motivated by applying a software engineering principle to an aspect of the architectural elements. You choose constraints; properties follow.
The summary slide contrasts them:
Concerned with logical organisation, possibly over time.
Concerned with component placement in a distributed setting. It deals with spatial distribution.
The slides stop at the definition. Tanenbaum & van Steen [2017] name three families: centralised (client-server, possibly split into tiers across machines), decentralised (peer-to-peer, every node in the same role) and hybrid (e.g. edge-server systems). Thunk's cluster of identical workers is decentralised.
An architectural style is formulated in terms of four things:
A style classifies systems with the same sort of organisation, lets them be compared, and provides general patterns for design.
An architectural style is a coordinated set of architectural constraints that restricts the roles/features of architectural elements and the allowed relationships among those elements within any architecture that conforms to that style.
A style captures the essence of a pattern of interaction by ignoring the accidental details of the rest of the architecture. Like design patterns, styles are devised out of existing systems rather than invented. Four are identified today as the main ones for distributed systems, and the slides add a fifth:
Main architectural styles for distributed systems
The last two styles are described by what processes do not need, which gives two axes for comparing all five. Processes are referentially uncoupled when they communicate without referencing or knowing each other; the slides pair this with being uncoupled in space. They are uncoupled in time when they communicate without being active at the same time. The two are independent: a publisher need not know its subscribers, but a subscriber that is absent when the event propagates misses it. Hence the slides' “also uncoupled in time” for the shared data-space.
Pick a style to see where it sits, or answer the two questions for your own design (a Thunk steal request, say).
M8 closes with a frank assessment. Styles are approximative and maybe non-scientific ways to model systems, yet expressive and abstract enough to help distributed system engineering: a simple and solid start. But is that a well-grounded science? Can we prove theorems about architectures? What is the role of “math-like” formalisms such as process algebra?
Architectures are not enough:
Concurrency is the first source of complexity in distributed systems. Formal models of concurrent systems abstract away from physical location, as architectures do, but more formally. They are aimed at:
Of several approaches, the course takes process algebra.
A process is a series of actions or events. An algebra is a calculus of symbols that combine according to certain defined laws. A calculus is a system or method of calculation.
A process algebra is a formal description technique for complex computer systems, especially those with communicating concurrently-executing components.
Following Baeten [2005]: before process algebra, basically only Petri nets [Peterson, 1977] existed for concurrent systems. Formal reasoning mostly gave semantics (meaning) to programming languages, in three ways:
Early models saw behaviour as an input/output function. Automata theory then modelled a process as an automaton: states, and transitions between them. What was missing? Interaction, and systems. Process algebra deals with interacting, concurrent processes.
Process algebra can be seen as the study of the behaviour of concurrent/distributed systems by algebraic means.
“Algebraic” is meant literally: process algebras use the methods of universal algebra [MacLane & Birkhoff, 1967]. A process algebra is any mathematical structure satisfying the axioms given for the basic operators, and a process is an element of a process algebra (in Italian, more clearly, algebra dei processi). With the axioms you calculate with processes, though process algebra often crosses the boundaries of universal algebra.
Best-known process algebras [Bergstra et al., 2001]
ACP: axioms first, communication as a function γ on actions (the rules below are in its style). CCS: complementary actions a, ā synchronise into a silent τ; bisimulation is its reference equivalence. CSP: processes synchronise on shared events; its standard semantics compares traces and refusals (failures), not bisimulation.
Key ingredients shared by all process algebras [Bergstra et al., 2001]
Start from a set of atomic actions (a, b, …), each representing indivisible behaviour. Basic operators combine processes into systems [Baeten, 2005]:
x + y alternative composition: executes either x or y.x ; y sequential composition: executes first x, then y. Often written x · y.x ∥ y parallel composition: executes x and y concurrently, in parallel.Neutral elements are ignored for now. Precedence “typically goes from + (weakest) to ;”, so a ; b + c is (a ; b) + c. The slides do not rank ∥, so here it is always parenthesised.
Structural laws [Baeten, 2005]
| Law | Name in the slides |
|---|---|
| x + y = y + x | 1 · commutativity of alternative composition |
| x + (y + z) = (x + y) + z | 2 · associativity of alternative composition |
| x + x = x | 3 · idempotency of alternative composition |
| (x + y) ; z = x ; z + y ; z | 4 · right distributivity of + over ; |
| (x ; y) ; z = x ; (y ; z) | 5 · associativity of sequential composition |
| x ∥ y = y ∥ x | 6 · commutativity of parallel composition |
| (x ∥ y) ∥ z = x ∥ (y ∥ z) | 7 · associativity of parallel composition |
Any mathematical structure with three binary operations satisfying the above laws is a process algebra. Most typically such structures are expressed as automata, mostly called transition systems.
The seven laws can be extended with left distributivity: x ; (y + z) = x ; y + x ; z. What changes?
With both right and left distributivity, the moment of choice does not matter. a ; (b + c) equals a ; b + a ; c.
Without left distributivity, the moment of choice matters. After a, the first process still offers b and c. The second has already committed to one of them.
It matters once the environment interacts: a user wanting c after a always gets it from the first process, but may find it gone in the second.
Laws say which processes are equal; transition rules say what a process can do. Each rule reads “if the premises above the line hold, so does the conclusion below”. x a x′ means that x can execute a and then behave as x′. The symbol ✓ means successful termination.
An atomic action executes and terminates. A choice proceeds either way; the other branch disappears. A sequence proceeds one way: when x terminates, y is left. Parallel composition either interleaves (one side moves; if it terminates, the other remains) or lets both sides act together through a communication function γ that turns a pair of actions into one. The four communication cases differ in which sides terminate. Applied repeatedly to a term, these rules (an SOS) build its LTS.
Pick a preset or type a term (actions, +, ;, | for ∥, parentheses). The rules above build its LTS; each transition lists its rule. Fill compare with to test equal traces and bisimilarity.
Law 4 holds under the rules: (a + b) ; c and a ; c + b ; c are bisimilar. Left distributivity does not: a ; (b + c) and a ; b + a ; c share traces but branch differently. The rules build a branching-time algebra, consistent with the seven laws (for ∥, given a commutative and associative γ, as ACP assumes). That is the relation between the two views:
If every law is valid for the LTSs the rules produce, what you prove with the laws holds for the running thing. The explorer's verdict on law 4 is a small instance of that check.
Uses of process algebra [Baeten, 2005]
Behavioural relations make “same behaviour” precise. Trace equivalence compares action sequences (linear time). Bisimulation also matches every choice point step by step (branching time). An equivalence lets you swap a component for an equivalent one, or check a refined design against its specification. It checks a model; it does not by itself make the code correct.
Lessons learnt · for good
Lessons learnt · for not-so-good
Architectures cover placement but prove nothing; process algebra proves but ignores space. A full model needs both, plus time (Ch. 2) and space (Ch. 3).
Practise answering these out loud, about your project.
Software: components (worker, stealer, evaluator, dashboard), connectors (message passing between BEAM processes), data (computations as DSL terms, results). System: one worker per container in a Compose cluster, all peers. Name your constraints (no central scheduler, pure tasks) and the properties they induce.
At its core, direct requests: a stealer names a random peer and needs it alive, so it is coupled in space and in time. Each node is internally layered (application, BEAM, network). A dashboard that only listens to events would be event-based. Only a persistent shared store of results would add time uncoupling.
It models structure, not behaviour, and has no formal semantics, so behavioural properties are understood qualitatively, not demonstrated. Process algebra adds unambiguous terms, laws to calculate with, and rules that build an LTS.
Laws are axioms for proofs; transition rules are a reference for implementation. If the rules obey the laws, the implementation carries the proven properties. Show law 4 holding and left distributivity failing in the explorer.
a ; (b + c) the same process as a ; b + a ; c?Same traces, so equal in linear time (with left distributivity). Different in branching time, because the second chooses at a. The slides' seven laws and rules are branching-time.
If x a ✓ then x ∥ y a y: the terminated side vanishes. In the four communication cases the result is ✓, x′, y′ or x′ ∥ y′, according to which sides terminate.
a ; b and b ; a traces of a ∥ b are both acceptable.| Slides | Content | Here |
|---|---|---|
| M8 · Prologue | Motivation; disclaimer | §1 |
| M8 · Software arch. | Handling complexity; components & connectors I–II; what is a software architecture; elements; properties & constraints | §2 |
| M8 · Software arch. | Styles to classify systems | §3 |
| M8 · Styles | Definition; main examples; the five styles (I–III each) | §3 |
| M8 · Conclusion | Summing up; questions | §2, §3 |
| M9 · Prologue | Proving features; focus on concurrency; harnessing complexity | §4 |
| M9 · Basics | Basic concepts; before process algebra I–II; ACP/CCS/CSP; basic ingredients; axioms; history | §4 |
| M9 · Operators | Basic operators; basic laws I–II; choosing the laws I–II | §5 |
| M9 · Operators | Transitions I–II; operational vs axiomatic; uses I–II | §6 |
| M9 · Conclusion | Lessons learnt I–II | §7 |