Promela Verification

Topic: Programming

Experiment: noun a test, trial, or tentative procedure; an act or operation for the purpose of discovering something unknown or of testing a principle, supposition, etc.: a chemical experiment; a teaching experiment; an experiment in living.

Promela is a verification modelling language used to verify the correctness of various programming paradigms, ranging from distributed systems to complex algorithm verification. I am presenting this language to you so that you can conduct a simple experiment.

Most, if not all, programmers are familiar with the mutual exclusion (mutex) problem; if you have multiple concurrently-running systems, how can you ensure correctness of data modification? Here is a simple example:

Suppose your program consists of 3 phases: the non-critical (NC) phase, the wait (W) phase and the critical (C) phase. You can have multiple programs running concurrently, each in their own subphase. For example, if you have two programs running, P1 and P2, then at a specific example snapshot (at a given instant) of the runtime, P1 can be in its NC phase while P2 can be in its W phase; we will denote this {1:NC, 2:W}.

We labelled these phases as such to demonstrate the mutex problem; at any given moment, we want only one program to be in its critical phase. This means that no two (or more) programs are in their critical phase at the same time. Using the above notation with only two programs, we want to assure that the following snapshot is impossible: {1:C, 2:C}.

Various algorithms exist to ensure that mutex is respected and enforced, such as Peterson's 2-Process MUTEX Algorithm or Dekker's Algorithm. This is not news to anyone, and anyone who has had any experience with concurrent systems has probably encountered these.

However, as anyone who has had any experience with concurrent systems can agree, testing these algorithms can be a pain. Enter Promela.

I won't teach you Promela here, as I believe it is a language which is taught by experience, but I will tell you about its benefits. I was forced to learn Promela in a course which I did not want to take, and it has proven to be an invaluable tool in algorithm and system verification. While it is certainly not easy to learn and use, it almost provides direct proof that your algorithm works by allowing you to do certain things which might not be possible in other programming languages, such as atomicity constraints.

(Note for the wise: if you cannot do these things in other languages, than why is it useful to test them in Promela? Well suppose you develop a theoretical polynomial-time algorithm for the 3CNFSAT problem, and thus prove that P = NP, but that algorithm requires some atomicity constraints, then C++ cannot really be used to test it, whereas Promela can give you the tools required.)

For those wanting to learn Promela, multiple websites exist which provide everything you need to get started. Additionally, you would need an interpreter, SPIN (the Simple Promela INterpreter), which also provides real-time LTL formula checking with finite automata acceptance capabilities.

Oh, and the experiment I mentioned? Just take your favourite algorithm, and try to implement it in Promela!

If you have any questions, please feel free to post them in the comments section. Until then, stay cool readers!

- Snowman