Lectures 3 and 4 - 24th September 2019 Flashcards
PROMELA continued and linear-time properties
What do atomic code blocks do in PROMELA?
They execute without interruption; all other processes wait until they are finished to prevent inter-process interference.
What are the properties of communication channels in PROMELA?
Unidirectional, specified, synchronous or asynchronous, can have one or multiple senders or receivers
How do you open and use communication channels in PROMELA?
Specify with chan type, send with !, receive with ?.
What are do blocks in PROMELA?
loops that are only broken with a break, return, etc in their code body
How does nondeterminism work in PROMELA?
Give multiple options for an operation to perform as with an NFA; all options (states) are evaluated in verification processes.
What are some ops that can be performed on comms channels in PROMELA?
length, if empty, if full, wait for specific message, and where to write received messages
Can active processes have arguments? Why?
No as they start themselves, so nothing to pass the arguments to them
Why would it make sense for the init() process to have an atomic block?
You don’t want any active processes or passive processes it starts to interleave and interfere with the initialisation process
What are safety properties?
Formalised conditions to prevent unwanted behaviour or conditions from a system
What is the mutual exclusion property?
A safety property ensuring that at most one process is within a particular specified critical section of code
What are liveness properties?
Formalised conditions to ensure that some desired functionality will eventually be executed
What are the 3 main variants of liveness properties?
eventually: each process will eventually enter its critical section
repeated eventually: each process will enter its critical section infinitely often
starvation freedom: each waiting process will eventually enter its critical section
What are invariants?
A check made to ensure something is always of the same state or value: an example of a verifiable safety property which has to be true in all system states.
How are invariants implemented in PROMELA?
using the assert() method
What are labels in PROMELA?
A prefix to a statement that makes a particular location in a program’s code referenceable
How can you check where a process is in its code in PROMELA?
[]@ is true iff the th process with the name is at the label
How can you extract local variables from processes in PROMELA?
:
What is the safe termination system property?
A safety property that checks whether all processes have reached a valid end state at the end of execution.
What is livelock?
When threads or processes are unable to progress due to them responding to each other during resource starvation, being stuck in an infinite loop of trying to get the resource.
How can you check for liveness in SPIN?
Label locations in the program as acceptable end states and check the processes reach them
What is fairness?
The evenness of the likelihood that different threads are able to advance whatever they are doing
What is unconditional fairness?
Every process gets its turn infinitely often
What is strong fairness?
Every process that is enabled infinitely often gets its turn infinitely often
What is weak fairness?
Every process that is continuously enabled from a certain time instant onwards gets its turn infinitely often
