Homework 3 (Tools Tracks)

Testing the Demarcation Protocol in Verisoft

You must implement, and test using Verisoft, the Demarcation Protocol.

Demarcation Protocol

The demarcation protocol is a protocol used in database systems to enforce constrains on distributed databases while minimizing communication overhead.

We consider an instance of the protocol where there are two sites, called Site 0 and Site 1. Each site is selling tickets for the same concert, and at most N tickets can be sold. In order to enforce the constrain that the number of sold tickets is always no larger than N, the two sites use a demarcation protocol, as follows.

Each site is allotted a certain number of tickets that it can sell without interacting with the other site. Let these two limits be L(1) and L(2). The intention is that L(1) + L(2) = N, but this is only a "fuzzy goal": obviously in a distributed system we cannot ensure that L(1) and L(2) change simultaneously, so this equality will not always hold. Most likely, though, in your implementation L(1) + L(2) <= N should hold. Initially, set L(1) = L(2) = N/2.

Each of Site i, for i=1,2, must process two kind of transactions: ticket sales, and ticket returns (a person gives back the ticket and gets a refund). If the transaction does not cause the site to sell more than L(i) tickets, it can do so without communicating with the other site. Let also S(i) be the number of tickets that have been sold at site i=1,2.

If the transaction would cause the site to exceed its limit L(i) of tickets sold, then it issues the other site a request to increase L(i) by some amount G (G not necessarily 1: it can be more efficient to ask for more). If the other site (Site 1-i) can grant the request (when L(i-1) - S(1-i) is at least G), then it does so. If it cannot grant it in full, it may (at your discretion) try to grant it partially. In any instance, Site 1-i returns to Site i some amount of tickets that can be added to L(i), and Site i tries then to complete the transaction.

Implementation and Testing in Verisoft

Implement and test using Verisoft the above protocol. Each Site should consist of at least two threads: one thread that processes the transactions (buy and sell tickets), possibly asking for limit increases, and the other thread that responds to the other site's requests for limit increase. Threads at different sites should communicate through messages, not shared memory!

The properties you should verify are: absence of deadlocks, and S(1) + S(2) <= N. You may have noticed that, since Site 1 and Site 2 are implemented in different threads that share no memory, you cannot write "S(1) + S(2) <= N" as an invariant to be checked by Verisoft. My suggestion would be to implement a single process (a 5th thread) that acts as the customers, issuing buy and return transactions to Site1 and Site2. You can then use an assertion that states that this 5th thread never has more than N unreturned ticket.

Extension to Three Sites

Extend the above implementation and testing to three independent sites. When at Site i you need more tickets than L(i), you should ask both of the other sites for more seats (hint: watch for deadlocks!).

What to submit

Submit a tarball (as an email attachment), containing the directory in which there are your .c files (the models of the 2-site and 3-site protocols), along with the definition files for Verisoft (essentially, system_file.VS). Include a README file in which you explain what you did, whether it worked successfully, how you tested it, whether you found bugs, and how can I now test it on Verisoft. I should be able to run verisoft demarcation_2sites.c (and similarly for 3 sites) and see that it is free of errors (don't achieve this by setting the max depth of exploration to 1!). Comment the code well, as I will be reading it.