Please enable JavaScript.
Coggle requires JavaScript to display documents.
Programming Language Concepts (PLC) - Coggle Diagram
Programming Language
Concepts (PLC)
Structured Types
Type Safety
The combination of
preservation
and
progress
.
Stuck Term
A term that cannot evaluate any further and is not a value of the language
This is an error state.
Weak Preservation
A weak statement of type safety.
Programs do not change their type after run time.
A language satisfies this if the following holds for all closed well-typed terms E:
if |- E:T and E |v| V then |- V:T
This is the only solution for big-step semantic
Preservation
After every step of evaluation, programs do not change their type.
if |- E : T and E -> E' then |- E':T
This is not sufficient to describe type safety as if we have a broke type system that allows a stuck term to be well-typed, then this stuck term will trivially satisfy preservation as there are no reductions from the stuck term so types are preserved!
Progress
The program never gets stuck
If |- E:T then either E->E' or E is a value V
Types
Pair Types
Written T x U, represents structures in which data of both type T
and
U are present
Sum Types/ Variants/ Enumerations
Sum Types
Written T + U, represents structures in which data is either of type T
or
U
Constructed using
injections
Variant Types
Also known as tagged union
Similar to the Haskell data structure
<l1:T1, l2:T2, ln:Tn>
Enumerated Type
Syntactic sugar for a variant where all values are of the unit type
Bool Type
A type with two distinct elements; true and false.
Unit Type
A type with exactly one value. Usually written as
()
This the type of Java methods that take no parameters
Thunking
The operation of wrapping an expression with a function of unit type to suspend its evaluation
Unthunking
Essentially executing the thunked function
Tuples
A generalisation of the pair type, instead able to hold n different expressions instead of 2.
Record Types
A generalisation of the tuple type, essentially uses labels instead of indexes.
Guide to myself
A
pair
is two elements that can be different types
A
tuple
is two or more elements that can be different types.
A
record
is a tuple where each element has a label . Same as a python dictionary
A
variant
is like the Haskell data type where a value can be one of multiple different labelled types
List Types
An ordered set of elements, all of the same type
Destructors
Operations that break structured types down
i.e. for pairs you have
fst
and
snd
, these are called
projections
Subtyping
Formally, subtype polymorphism. Subtyping is the process of assessing whether a subtype (some datatype) is related to a supertype such that functions written for the supertype will also work for the subtype
Structural Subtyping
Analysing the capabilities of the types and saying that T is a subtype of U if all the operations that can be performed on U can also be performed on T
Record Subtyping
Depth Subtyping
A record A can be a subtype of another record B if the type of each of its values is a subtype of a corresponding value in B
Width Subtyping
Extra fields may be added to the subtype
Permutation Subtyping
Listed fields may be re-ordered
Variant Subtyping
Depth Subtyping
Same as record
Permutation Subtyping
Same as record
Width Subtyping
Opposite to record-- extra fields may be added to the
supertype
Nominal Subtyping
Explicitly declaring which types are subtype of others and then making sure than any operations valid on a supertype are valid on the subtype
Subtyping Relation
This is often not enough, also need to provide rule that the relation is
reflexive
and
transitive
Typically, inheritances forces that every member in the supertype also exists in the subtype.
Subsumption
If T is a subtype of U, then every value of type T can also be considered as a value of type U.
Subtyping Relation
T <: U
means T is a subtype of U
Covariance
Covariant Type Former
A type former in which the order of types in the subtyping relation is preserved
Contravariant Type Former
This best explained through example.
Say that we have a type former call
Foo
, and that given a type
T
, then
Foo T
is a new type. If subtyping
Foo
is such that
T <: U
then
Foo U <: Foo T
, then
Foo
is a
contravariant
type constructor
For different types
Lists
Covariant
Functions
Return: Covariant
Arguments: Contravariant
Arrays
Invariant
Read: Covariant
Write: Contravariant
Syntax to Execution
Types
Reasoning about programs
Semantics
Of a programming language is a specification of how each language construct affects the behaviour of programs written in that language
Denotation Semantics
Maps every program to a point in a mathematical structure that represents the values that the program calculates
ie. [[if 0<1 then 0 else 1]] = 0
Semantic Domain
The set of elements that can represent the meaning of a program.
e.g. 1: For a program that only output positive integers, the domain can be the set of natural numbers
2: For programs that represent functions from ints to ints, the semantic domain would be the set of all functions from naturals to naturals
Denotation Function
The mapping from constructs in the language to elements in the semantic domain
[[true]]o =
true
[[false]]o =
true
[[n]]o =
n
(where n is a natural number)
[[x]]o =
v
(where o maps x to v)
[[E < E']] =
true
(If [[E]]o < [[E']]o)
Operational Semantics
A relational approach that typically uses inductively defined relations between either programs and the values they produce or the different states a program can transition between
e.g if 0<1 then 0 else 1 [is mapped to] -> if true then 0 else 1
Big Step
Where the binary relation is between terms and values; representing the values that a term can evaluate to.
Small Step
Gives an inductive relation between terms representing run time states of programs.
Axiomatic Semantics
The meaning of a program is the properties you can prove of it using a formal logic (e.g. Hoare logic)
Semantics of Concurrency
First Principles
Thread
A single executing sequence of control
For threads to interact, they must be able to synchronise
Therefore, they must be able to send signals to other threads and recognise when signals have been sent to them
Synchronisation Paradigms
Signal and Wait
A thread that signals another thread sends its signal and then enters a waiting state so that it cannot be scheduled further until the signal is received.
Aka
Synchronous communication
(threads need to rendezvous)
Signal and Continue
A thread that signals to another thread does not need to wait until the signals is received-- it may continue its execution immediately after signalling.
Aka
asynchronous communication
(sending threads do not need to rendezvous)
Process Calculus
A diverse set of approaches for formally modelling concurrent systems
Calculus of Communicating Systems (CCS)
Devised by Robin Milner around 1980
Grammar
P ::= nil | a ! P | a ? P | t P | P||P | P \ a | X | | rec X . P
nil
is an inert process - it has terminated
a ! P
sends a signal on a channel named '
a
' and then continues execution as
P
a ? P
receives a signal on a channel names '
a
' and then continues execution as
P
t P
takes an internal computation step
P || P
represents two concurrent processes, this models thread spawning as well
P \ a
is a restriction operation - no communication on channel
'a'
originating inside of
P
can be seen
X
and
rec X . P
are used for recursive behaviour, e.g. rec X . a ! b ? X, is a process that repeatedly sends a signal on 'a' and receives a signal on 'b'
Asynchronous CCS
P ::= nil |
a ! nil
| a ? P | t P | P||P | P \ a | X | | rec X . P
Communicating Sequential Processes (CSP)
Devised by Tony Hoare
Includes broadcast communication
Semantics denotationally presented as opposed to the small step operationally presented semantics of CCS
Communication Mechanisms
Handshake Communication
Where a single sender and receiver communicate when the sender is ready to send and the receiver is ready to receive
Broadcast Communication
Where a signal is sent to all concurrent processes that are ready to receive that signal, not just a single process.
Labelled Transition Systems
Used to represent the tree of transitions for the non-deterministic behaviour of threads
Formal Definition
An LTS is a mathematical structure (X, Σ, L) where:
X is a set of states
Σ is an alphabet of actions
L is a subset X x Σ x X ie (before state, transition, after state)
Example
Diagrammatically
Formally
X = {s0, s1, s2, s3}
Σ = {"x is 0", "x is 1", "x is 2"}
L = {(s0, "x is 0", s1), (s0, "x is 1", s2), (s0, "x is 2", s3)}
Essential Aspects of Concurrency
Communication
Processes communicate with other processes either through shared memory or message passing
Synchronisation
Processes must sometimes synchronise their actions to ensure atomicity
Non-determinism
What can be observed about a program changes from one run to the next
Kinds of Non-Determinism
Internal
"The machine chooses"
i.e. the nondeterminism is resolved by the scheduler
External
"The environment chooses"
i.e. the combination of a vending machine and user can be thought of as a concurrent system
Process Equivalence
Trace Equivalence
Two states are trace equivalent when they have the same traces
Simulation Equivalence
States x and y are said to be simulation equivalent if both x<=y and y<=x
Simulations
Formally
Suppose that (X, Σ, L) is a labelled transition system
A simulation is a relation on the states that satisfies the following condition:
Whenever xRy and x -a-> x' then there exists y' such that y -a-> y' and (x', y') in range of R, i.e. x'Ry'
If xRy, we say that
y simulates x
We sometimes write x <= y if there exists a simulation that contains (x,y)
Properties
Union
Unions of simulations are simulations
The union of all simulations =
the largest simulation
The largest simulation, written <=, is called
similarity
Simulation is an instance of something called coinduction
How to show that y simulates x?
Construct a simulation that contains the pair (x,y)
How to show that y does not simulate x?
Demon game >:D
Start at position (x, y)
The demon picks a move x-a->x'
We must choose a y' such that y-a->y'
The game goes back to the demon's step, changing the position to (x', y')
If at any point a player cannot make a move, that player loses
If the Demon has a winning strategy, then y does not simulate x
If we have a winning strategy, then x<=y (y simulates x)
Intuitively
Whenever x can do an action to become x', y can do an action to become y', and same so x' and y' recursively
Bisimulation Equivalence
Bisimulations
Intuitively
A simulation that goes both ways-- that is the relation and its reverse are both simulations
Formally
Suppose that (X, Σ, L) is a labelled transition system
A bisimulation is a relation on states that satisfies the following conditions, whenever (x,y) in range of R
If x-a->x' then there exists y' such that y-a->y' and (x', y') in R
If y-a->y' then there exists x' such that x-a->x' and (x', y') in R
We write x~y if there is a bisimulation that contains (x, y)
Properties
Union
The unions of bisimulations are bisimulations
The largest bisimulation is the union of all bisimulations and is written as ~ and called bisimilarity
How to show a bisimulation between x and y
How to show there is not a bisimulation between x and y
Demon game >:D
Start at position (x,y)
The demon picks where to play, either at x or y
If the demon chose x, he picks a move x-a->x'
In this case, we must respond with y-a->y'
The demon chose y, he picks a move y-a->y'
In this case, we must respond with x-a->x'
The game goes back to step 1, changing position to (x', y')
If, at any point, the player cannot make a move, the player loses
If the Demon wins, then x and y are not bisimilar
If we win, then x ~ y
Concurrency in programming languages
Concurrency Models
Shared Memory Concurrency
Definitions
Processes
An operating system abstraction, includes:
An address space
A number of threads
each with own call stack
Threads within a single process share an address space so can communicate via
shared memory
Threads can read and write to memory via a local cache
On multi core systems, threads write to
different caches
Cache synchronisation is computationally expensive so writes to main memory (heap) may not take effect immediately
Threads on different cores will not see other's writes until the caches are flushed to main memory
Context Switch
The operation of switching control from one thread to another.
Happens at the machine level
A context switch can happen in the middle of a "high-level" operation, e.g. assignment to a variable
Thread Life Cycle
New
(Gets
admitted
to ready)
Ready
(Gets
scheduler dispactched
to running)
Waiting
(Gets
I/O
or
event completion
to ready)
Running
(Gets
exited
to terminated)
(Gets
I/O
or
event waited
to waiting)
(Gets
interrupted
to ready)
Terminated
Race Condition
The situation in which two or more threads are simultaneously trying to write and read-or-write from shared memory
Two factors required for race conditions to occur
Aliasing
Same location in shared memory (heap) accessible from multiple threads
Mutability
Data on the heap can be altered
This can't happen simultaneously, so one thread will end up writing or reading before the others
In the absence of any other control, it is the thread scheduler that decides which
Visibility
An operation by one thread is visible in another thread if its effect can be seen via main memory
Can be forced in Java with keyword volatile
Fundamental Communication
The sending thread must write a message in to a memory location
The sending thread notifies any receiver threads that it has done so
The receiving thread reads the message from the same shared memory location
For synchronous communication, the receiving thread notifies the sender that it has done so
Mutual Exclusion
and
Critical Regions
Critical Region
Parts of program where a shared resource is access. Importantly where a shared resource is modified.
Mutual Exclusion
If one thread is in its critical region for a resource, then no other threads are allowed to enter their critical region for that resource
Solutions
Boolean Lock
NOT A SOLUTION
Taking Turns
Guarantees mutual exclusion
But forces alternation which is really inefficient
Peterson's Algorithm
Mixes the idea of boolean locks and turn taking to guarantee mutual exclusion, blocked threads and avoids unbounded waiting for other threads
Uses and interested table and a turn variable
Broken
on modern computers and compilers and hardware
reorder instructions
within individual threads
This is done consistently so that each individual CPU still follows the logic of the original
However, the order in which one thread sees changes in memory made by another thread on a different CPU may not follow the logic of the source
Memory Barriers
(aka fences)
Machine level instructions that are used to help with problems due to re-ordering
They preserve the externally visible program order between CPUs
They make memory visible by causing cache propogation
A point at which instructions shouldn't be reordered past
Atomic Operations
Provided by the hardware, allow for testing and setting of a lock as a single, uninterruptible operation
Test-and-set Lock (TSL)
Instruction
TSL RX,LOCK
Reads the value of memory location
LOCK
Writes the value to register
RX
Stores a nonzero value at
LOCK
Guaranteed to be indivisible, memory bus is locked for the duration of operation
Compare-and-set (CAS)
A similar operation sometimes given as a language primitive called CAS
Used for programming fine-grained concurrent algorithms
Uses TSL
XCHG
Exchanges two register and memory locations atomically
Used for similar purposes as
TSL
Busy Waiting
Spinning on a loop, checking the locks and variables, rather than doing nothing
Locks
Java
ReentrantLock
tryLock()
allows for a non-blocking attempt to acquire the lock
lockInterruptibly()
allows for an attempt to acquire the lock but allows the block thread to be interrupted
getQueuedThreads()
returns the Collection of threads currently waiting on the lock
However
, the client code using these locks is responsible for both acquiring and releasing the lock. This can be dangerous
Concepts
Lock Overhead
It takes computation cycles to test, wait and acquire, and release lock. Using locks often to protect many small areas of code increases overhead.
Lock Contention
Situations in which one thread is trying to acquire a lock whilst another holds it. Using locks less frequently but protecting larger blocks of code increases the risk of contention.
Granularity
The trade-off between overhead and contention
Fine-grained concurrency
Systems with more locking of small blocks of code
Coarse-grained concurrency
Systems with fewer locks over larger blocks of code
Intrinsic Locking
Implicit locking rather than explicit locking
Refers to identifying blocks of code that should be protected with a mutex lock.
In Java,
synchronised
Monitor
wait()
method
notify()
method
notifyAll()
method
Message Passing Concurrency
Advantages
No need to worry about critical regions and mutex locks
Run less risk of deadlock as we aren't necessarily holding locks
Avoid problems with cache visibility as we know which thread is the intended recipient of the message
Can use a distributed system model
Well established interfaces (e.g. MPI) and well studied theory
Disadvantages
Much slower
An unnecessary higher level API that you don't need if you can program well
Synchronicity Models
Synchronous
Synchronous message passing (sender blocks until receive is ready) is popular for hardware design languages, and is easier to program with but is difficult (and at worst, impossible) to arrange in a distributed system
Asynchronous
Asynchronous message passing (sender does not block, messages are buffered) is the popular choice for distributed applications.
Difficult to program for:
Typically the idiom is to send a message and set up a receiver for a callback when the message is received
Callbacks appear "non-linearly" in the program flow and do not help with maintainability and debugging.
The flow of messages controls the program flow
Channels
Handshake
A message between just two threads
Multicast
A message between many threads
Broadcast
A message to all threads in the system
The Actor Model
A variation of MPC
Actors
All computation is performed by Actors
Actors do not share memory
Actors have unique addresses to which they can be sent messages
Actors have a thread of control
Actors have a "mailbox" that acts as a FIFO queue for incoming messages
Actors can send messages, or values, to other actors and receive messages from their own mailbox
Actor Messages
Messages consist of value-- these can be typed or untyped
Values can include the address of other actors-- this means the underlying communication topology is dynamic
In response to receiving a message, an actor can:
Send a finite number of messages to other actors
Create, or spawn, a finite number of new actors
Change its own behavioural state
Actors communicate "locally" this means actors only send to other actors for which
They already know the actor's address
They have received the actor's address in a previous message
They are the creator of the actor
Hierarchical Actors
Each Actor has a unique parent Actor who created it and the parent supervises various features of the behaviour
E.g. parents can delegate actions to its sub-Actors
Error handling could be handled hierarchically
Failures in lower Actors can be passed up to higher Actors if not failed
Error Handling
Strategies
All For One
Handler applies to all children
One For One
Handle applies to failed children only
Handler Actions
Resume
Restart
Stop
Escalate
Coroutines
Definition
A generalised subroutine where you don't fait for the subroutine to complete before proceeding
Threads vs Coroutines
Concurrency and Parallelism
Coroutines allow for concurrency but not parallelism
Threads allow for concurrency and parallelism
Multi-Tasking Style
Coroutines provide the benefits of programming in a
cooperative
multi-tasking style. Coroutines know exactly the control points where they will yield the processor
Threads are designed for
pre-emptive
mutli-tasking. Threaded code does not know when it will be interrupted and yield the processor
Thread Pools, Promises and Futures
Thread Pools
An object that manages thread creation, destruction, priority and scheduling. It controls a set of threads that is abstracted from the programmer who just submits a task to the thread pool.
Java
Executor
Base thread pool
ExecutorService
A thread pool with extra services
Thread to System Thread Mapping
Single-Threaded Pools
Executors.newSingleThreadExecutor
Cached Pools
Executors.newCachedThreadPool
Fixed Size Pools
Executors.newFixedThreadPool
Work Stealing Pools
Executors.newWorkStealingPool
Scheduled Pools
Executors.newScheduledThreadPool
Pros and Cons
Pros
Removes the onus of thread management from the user
Removes the overhead of thread creation and start time whenever a thread is re-used
Efficient and correctly started thread management code
Cons
Risk of deadlocks in fixed size pools that are too small
Risks of excess overhead for thread pools that are too large -
resource thrashing
Risk of
thread leakage
if a thread throws an exception that is not handle properly. It can be removed from the thread pool and effectively shrinks the size of the pool
Methods
Submit Method
Inside ExecutorService, rather than Executor which just has execute()
Similar to
execute()
but provides a mechanism for determining when the task has completed
It does this by returning a special object that tracks progress of the task in the thread pool
This object can be used to cancel execution of the task after the task has been deployed but not yet completed
Futures
Wrapper for a place where a computation will store its result
in Java
Methods
boolean cancel(boolean mayInterruptIfRunning)
V get() // blocks until value is placed in future
V get(timeout)
boolean isCancelled()
boolean isDone()
Promises
A write-once container that behaves like a Future.
You are promising that YOU will write into at some point
Impetus
Futures are read only
Performance
Performance Measures
Responsiveness
Time until first response from a task
Throughput
Tasks per unit time
Scalability
The ability to increase performance by increasing the number of system resources
Clock-speed
More memory (avoid thrashing)
Bigger cache sizes (fewer cache misses)
Amdahl's Law
A guide for measuring theoretical limits on system performance based on parallel execution of a fixed task
speedup <= 1 /(F + (1- F) / N)
where F is the fraction of a task that is sequential and let N be the number of processors available
Derivation
Assume
T
is time taken to execute a task
Then
T
can be written as
T = FT + (1-F)T
If we use N processor, then theoretically the parallel portion can be revised to
(1-F)T / N
Therefore revised execution time =
T' = FT + (1-F)T / N
Therefore speed up
= T / T'
= Amdahl's Law
Lock Contention
The problem of multiple threads competing for the same lock
Reducing lock contention can help by
Reducing duration for which locks are held (fine grained concurrency)
Reducing the frequency at which locks are request
Replace mutual exclusion locks with other coordination mechanisms
Lock Free Algorithms
Compare and Set (CAS)
CAV ( V, A, B )
V is a memory reference
A is the old value stored in the reference
B is the new value to store in the reference
Treiber Stack
Exponential Backoff
Each process should have a variable backoff time after failing compareAndSet to reduce contention
Elimination Array
i.e. if there are two threads; one trying to push and one trying to pop, just return the push value to the pop without touching the stack
