Modelling Complex Software Systems

Concurrency

A design principle for potential parallelism that allows multiple tasks to be completed at once

Interference

Data is accessed in an uncontrolled manner by multiple processes

Deadlock

Two processes cannot progress because their progression is dependent on resources that the other is holding

Safety

Concurrency principle that states “nothing bad will ever happen”

Liveness

Concurrency principle that states “something good will eventually happen”

Thread

Java class for representing a process

run()

Java method containing what a process actually does (should not be called directly)

o.start()

Java method that calls .run() on process o

sleep(long ms)

Java method that suspends a thread for a given time

yield()

Java method that pauses a current thread

t.join()

Java method that suspends the caller process until t is complete

Semaphore

Data structure used to track and synchronise access to a resource. Consists of the number of available permits and set of waiting processes

S ← (k, {})

Semaphore initialisation value

synchronized

Java keyword for synchronising methods and objects

volatile

Java keyword that prompts the machine to reload a value without caching

Monitor

Data structure that manages concurrency by encapsulating the responsibility for managing the data with the object that owns it.

wait()

Java method used to pause a process until it is notified

notify()

Java method used to wake up a single thread that is waiting for a lock

notifyAll()

Java method used to wake up all threads that are waiting for a lock

interrupt()

Java method used to pull a thread out of a non-active state (e.g. waiting/sleeping)

Finite State Processes

Modelling language for concurrent programs

ERROR

Goes to FSP state -1

STOP

Goes to FSP deadlock state

END

Goes to FSP E state

property

FSP keyword for safety

progress

FSP keyword for liveness

fluent FL = <{s1, …, sN}, {e1, …, eN}> initially 1

FSP fluent structure

assert ALWAYS_F = []F

FSP check that F is always true

assert EVENTUALLY_F = <>F

FSP check that F is eventually true

assert F_UNTIL_G = F U G

FSP check that F is true until G turns true

Dynamical system

Mathematical model that describes how a system evolves over time. Made up of a state space, update rule and initial condition

Logistic map

Formula for computing the change in population over discrete time steps

[0, 1)

Logistic map: r value for which population decreases

[1, 2)

Logistic map: r value for which population linearly approaches equilibrium

[2, 3)

Logistic map: r value for which population oscillates towards equilibrium

[3, 3.45)

Logistic map: r value for which population oscillates between 2 values

[3.45, 3.57)

Logistic map: r value for which population increasingly oscillates between >2 values

[3.57, 4)

Logistic map: r value for which population is chaotic with windows of stability

[4, inf)

Logistic map: r value for which population is fully chaotic

Butterfly Effect

Two states with imperceptibly different amounts produce wildly different outputs

Bifurcation diagram

Graph that maps r value onto convergence value of logistic map.

Ordinary Differential Equation

Mathematic model that uses macro-equations to model the rate of change of a system

Lotka Volterra Model

Model of predator prey numbers

gamma

LV: death rate of foxes

delta

LV: rate that foxes turn rabbits (food) into foxes (reproduction)

alpha

LV: rabbit growth rate

beta

LV: rate that foxes eat rabbits

transient

Model behaviour when it moves towards a state

fixed point

Model behaviour when it reaches a steady state

limit cycle

Model behaviour when it oscillates

class 1

Wolfram class that rapidly converges to uniform state

class 2

Wolfram class that rapidly converges to repetitive state

class 3

Wolfram class that appears to remain chaotic

class 4

Wolfram class that appears to remain chaotic with periods of stability

Rule 110

Turing complete 1D cellular automaton rule

Von Neumann

2D CA Neighborhood that doesn’t include diagonals

Moore

2D CA Neighborhood that does include diagonals

Loneliness

Game of life rule that kills a cell with <2 neighbours

Overcrowding

Game of life rule that kills a cell with >3 neighbours

Survival

Game of life rule that sustains an existing cell with 2-3 neighbours

Reproduction

Game of life rule that produces a new cell with 3 neighbours

Separation

Feature of Boids Model of Flocking Behaviour that prevents collisions

Cohesion

Feature of Boids Model of Flocking Behaviour that provides safety in numbers

Alignment

Feature of Boids Model of Flocking Behaviour that keeps boids moving in the same direction

Self-contained

Essential agent feature: has boundary

Autonomous

Essential agent feature: acts for itself

Dynamic state

Essential agent feature: attributes change over time

Social

Essential agent feature: interacts with others

Adaptive

Optional agent feature: learns from the past

Goal-directed

Optional agent feature: wants to achieve something

Heterogeneous

Optional agent feature: has different types

Reachable

A marking that can be reached from the initial marking

Final

A marking in which no hot transitions are enabled

epsilon

symbol for cold transitions (external to system)

phi

symbol for silent transitions (not visible to observer)

sequential run

Sequence of steps from initial marking

complete sequential run

Sequential run that leads to a final marking or cannot have any addition steps inserted

state explosion problem

Rapid growth of marking graph when adding tokens

interleaving semantics

List of all complete sequential runs

Distributed run

Acyclic net representing a series of steps towards a marking.

Boundedness

Set of all reachable marking is finite

k-boundedness

For all reachable markings, there are no places with > k tokens

safety

For all reachable markings, there are no places with multiple tokens

liveness

From every possible reachable marking, we can reach a marking that enables a transition

deadlock-freedom

Every reachable marking enables at least one transition

workflow net

Petri net with source place (•x = {}) and sink place (x• = {})

workflow system

A workflow net and initial marking that puts one token in the source (and nowhere else)

Option to complete

For every reachable marking, we can find a way to place a token in the sink

Proper completion

If we place a token in the sink, there is only one there and none elsewhere

No dead transitions

Every transition can be enabled by a reachable marking

Soundness

Option to complete, proper completion and no dead transitions