Bank loans

In this exercise we will play with a variation of a classical example of concurrency problem proposed by E. W. Dijkstra in 1982 that led to the design of the Banker's algorithm. We will use here the simplest case where the Banker's algorithm is not being applied.

A given bank with an initial capital CAP>0 of money has N>0 clients. Each client i is allowed to ask for loans up to a given predefined maximum max[i] of total loan where 0<max[i]<=CAP. The client may return all the money borrowed so far at any moment. On the other hand, once a client reaches its maximum loan, it cannot ask for further money so she can only return her money in a finite time, cancelling the loan.

Implementation in Promela

We will model each client as a different process. The bank will not be modelled: instead, each client will withdraw from the bank cash the money she requests, whenever she gets the chance. We will fix N=3 clients and define the following structures:

//Global variables #define N 3 #define CAP 10 short max[N]={2,4,3};     // Maximum money needed by each client short loan[N]=0;          // Current amount lent to each client short cash=CAP;           // Money in the bank (initially, the capital CAP)

The client can do one of the following operations:

1. If the client has not reached her maximum loan, she can request any arbitrary amount from 1 euro to the remaining money to get her maximum loan. When a money request is chosen, the program will do the operation
   
   req:  printf("C%d requests %d.   %d:[%d,%d,%d]\n", _pid, request, cash, loan[0],loan[1],loan[2]);
   
   to inform about her wish to get more money. Note that this printf has the label req. An example would be:
   
      C1 requests 2.   6:[2,1,1]
   
   The client will wait until there is enough cash, and proceed to take her request, adding it to her current loan. When the client gets the requested money, she also prints a message like
   
      C1 got the money 2.   4:[2,3,1]
   
   
2. If the client has any loan greater than 0, she can return it at any moment. When doing so, it will make a printf like, for instance:
   
      C1 returns its loan 3.   7:[2,0,1]

Warning 1: any money transfer (either an income or a payment) implies modifying the cash and the client's account loan[i]. Since both modifications cannot be done in a same assignment, you will have to guarantee that the two operations are blocked in such a way that no other process can make changes to those variables in the middle of the transfer.

Warning 2: when you run SPIN in verification mode and execute the program analyzer pan pay attention to error messages of the form

  error: max search depth too small

If this happens, there might be errors not detected, so try to increase the search depth using the option -m like, for instance, in:

  ./pan -m1000000

Goals

We will prove the following properties trying with different input configurations:

1. absence of deadlock: we cannot reach a state in which all clients get blocked requesting more money and the bank has not enough cash to lend.
   
• Make tries with CAP=10 and lower. Obviously, if we start CAP=0 we will get a deadlock (there is no initial money at all). Find the maximum CAP value x for which you can get a deadlock.
  
• Get some deadlock trace for CAP=x and explain it: focus on the last operations of each process and the current status of the cash and the clients' accounts.
  
  
2. safety: fixing CAP=x+1 check the following properties
• the cash is always between 0 and CAP
• each account loan[i] is always between 0 and max[i]
  
• after each bank transfer, check that the sum cash+loan[0]+loan[1]+loan[2] is equal to CAP (note that, during the transfer, this may be momentarily violated). You can simply use an assert for this property.
  
  
3. liveness (lack of starvation): check if for any client i, when she makes a request, she will eventually get a payment. Use instruction labels to name the points in the code where a request and a payment is done. If you find a counterexample (that is, at least one client not satisfying this property) explain the obtained trace.
   

Assessment & delivery