0.3 Modeling concurrent processes  (Page 17/21)

The moral of the story is that concurrent protocols can difficult and subtle. The SPIN book puts it well:The number of incorrect mutual exclusion algorithms that have been dreamt up over the years, often supported by long andpersuasive correctness arguments, is considerably larger than the number of correct ones.[ One exercise ],for instance, shows a version, converted into Promela, that was recommended bya major computer manufacturer in the not too distant past.

The following are some other ideas, each of these can form the kernel of a successful mutex algorithm.

• First-come, first-served. Within Promela/SPIN, we assume onestatement is executed at a time, so processes must arrive at the critical section in some particular order.
• Pre-determined priority order, e.g. , by process ID.
• Least recently used. I.e. , processes defer to others that haven't recently executed this code.
• Random. E.g. , each process randomly chooses a number, withties broken randomly also.

Issues in writing feasibly-verifiable programs (optional)

Banking

Our first Promela examples were drastically simplified models of banking, with deposits and withdrawals. Now, let's considera production-quality system of bank accounts. Its code base could easily entail millions of lines of code.

Before we start porting the entire system to Promela, let's consider what it is we want to use SPIN to verify.Ideally, we want to verify everything, including ensuring that each account balance is correct. But, think aboutthat in conjunction with SPIN's approach using state spaces.

Even with only one bank account, if we model balances accurately, we need an infinite number of statesone for each possible balance. Similarly, the production system likely has no boundon the number of possible accounts. SPIN would have a wee bit of difficulty searching theentire state space in finite time. To make verification feasible, all SPIN models are requiredto be finite. (All data types, including int , have a finite range.)

How could we restrict the Promela program to guarantee finiteness?The most obvious and least restrictive option is to simply use the int type and ensure that any examples used should not cause overflow.

To make verification efficient, the state space should berelatively small. Even using int s as bank balances andaccount numbers, assuming only 1000 lines of code and ignoring any other program variables, we still have $2^{32}{2}^{32}\times 1000$ statesover 18 sextillion. Even at a billion states per second, averification could still take over half a millenium!

Let's abandon the goal having our Promela prototype track the particular balances accurately.Since our focus is on concurrency, we mainly want to ensure that when there are multiple simultaneous transactions, we don't loseor mix up any of the data. We might also want to verify the securityprotocols used in selecting appropriate accounts. But, we no longer need to even keep track of balances.Furthermore, it is highly unlikely that the production code might have errors that only occur when there are a large numberof accounts, so we can comfortably use just a few.