Lectures 3 and 4 - 24th September 2019

Question 1

What do atomic code blocks do in PROMELA?

Answer 1

They execute without interruption; all other processes wait until they are finished to prevent inter-process interference.

Question 2

What are the properties of communication channels in PROMELA?

Answer 2

Unidirectional, specified, synchronous or asynchronous, can have one or multiple senders or receivers

Question 3

How do you open and use communication channels in PROMELA?

Answer 3

Specify with chan type, send with !, receive with ?.

Question 4

What are do blocks in PROMELA?

Answer 4

loops that are only broken with a break, return, etc in their code body

Question 5

How does nondeterminism work in PROMELA?

Answer 5

Give multiple options for an operation to perform as with an NFA; all options (states) are evaluated in verification processes.

Question 6

What are some ops that can be performed on comms channels in PROMELA?

Answer 6

length, if empty, if full, wait for specific message, and where to write received messages

Question 7

Can active processes have arguments? Why?

Answer 7

No as they start themselves, so nothing to pass the arguments to them

Question 8

Why would it make sense for the init() process to have an atomic block?

Answer 8

You don’t want any active processes or passive processes it starts to interleave and interfere with the initialisation process

Question 9

What are safety properties?

Answer 9

Formalised conditions to prevent unwanted behaviour or conditions from a system

Question 10

What is the mutual exclusion property?

Answer 10

A safety property ensuring that at most one process is within a particular specified critical section of code

Question 11

What are liveness properties?

Answer 11

Formalised conditions to ensure that some desired functionality will eventually be executed

Question 12

What are the 3 main variants of liveness properties?

Answer 12

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

Question 13

What are invariants?

Answer 13

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.

Question 14

How are invariants implemented in PROMELA?

Answer 14

using the assert() method

Question 15

What are labels in PROMELA?

Answer 15

A prefix to a statement that makes a particular location in a program’s code referenceable

Question 16

How can you check where a process is in its code in PROMELA?

Answer 16

[]@ is true iff the th process with the name is at the label

Question 17

How can you extract local variables from processes in PROMELA?

Answer 17

:

Question 18

What is the safe termination system property?

Answer 18

A safety property that checks whether all processes have reached a valid end state at the end of execution.

Question 19

What is livelock?

Answer 19

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.

Question 20

How can you check for liveness in SPIN?

Answer 20

Label locations in the program as acceptable end states and check the processes reach them

Question 21

What is fairness?

Answer 21

The evenness of the likelihood that different threads are able to advance whatever they are doing

Question 22

What is unconditional fairness?

Answer 22

Every process gets its turn infinitely often

Question 23

What is strong fairness?

Answer 23

Every process that is enabled infinitely often gets its turn infinitely often

Question 24

What is weak fairness?

Answer 24

Every process that is continuously enabled from a certain time instant onwards gets its turn infinitely often

Question 25

What variants of fairness can SPIN check for?

Answer 25

weak fairness

Question 26

What are SPIN, ISPIN, and PROMELA, and how are they related?

Answer 26

SPIN is a general tool for the logical verification of concurrent software in a rigorous and mostly automated fashion.

ISPIN is a GUI for SPIN.

PROMELA is a verification modeling language used with the SPIN tool.