Project
The 1-week goal is for each team to develop, and describe on the wiki, the architecture of their component. In particular:
- The DB team should put up a description of the DB schema, and a tentative list of methods that they will provide.
- The Email team should study how to interface to Exim, and have some proposal for how to authenticate the sender of the emails.
- The Web team should have a proposal on how the user will navigate through the pages (the simplest, the better), and how to interface to the DB.
The 2-week goal will consist in developing precise interfaces for these components. Turn in the assignment in the wiki.
Reading
Read lecture 3 and lecture 4 on Verisoft, as well as the POPL 97 paper. Of the lectures, you don't need to study every detail: you just need to be familiar with what we covered in class.
Problem Set
The following problems are related to Verisoft. Please turn in solutions on sheets of paper, stapled together; write your name on your assignment.
Problem 1: Dining Philosophers
Consider an instance of the dining philosophers problem with n philosophers, numbered 0, ..., n-1. Between philosophers i and i+1 mod n is chopstick i, and there are two operations on the chopstick:
grab_j(i) philosopher j grabs chopstick i (where j = i or j = i+1 mod n); the chopstick has to be on the table for this to be enabled, and the effect is that the philosopher is holding the chopstick afterwards.
release_j(i) philosopher j releases chopstick i (where j = i or j = i+1 mod n); this is enabled if philosopher j is holding the chopstick i, and the effect is that the chopstick will be on the table afterwords.
Give the independence relation I. For independence, use the definition at page 18 of lecture 3.
Problem 2: Talking Philosophers
Consider an instance of the talking philosophers problem with n philosophers, numbered 0, ..., n-1. Between philosophers i and i+1 mod n is a channel C_i, so that i can talk to i+1 mod n. Each channel can hold at most 4 messages, and is organized as a FIFO. There are two operations on the channel:
send_i(i) philosopher i sends a message on channel C_i, for 0 <= i < n
recv_j(i) philosopher j receives a message from channel C_i (where j = i+1 mod n).
Consider the state s, where each channel contains exactly two messages, and consider the dependency table between send and recv given at page 27 of lecture 3. Is there a persistent set T that is neither empty, nor it consists of all transitions? Either give one such set, or prove that there is none.
Problem 3: Supping Philosophers
In this problem, there are again n philosophers, but each one of them has a soup dish in front. Each philosopher has a spoon, which can be either in the soup, or out of it. Basic table manners require that philosophers dip their spoons only in their own dishes. Thus, philosopher i, for 0 <= i < n has two operations on the dish:
dip_i(i): philosopher i dips the spoon into the dish (it can only be done if the spoon is out of the dish)
lift_i(i): philosopher i lifts the spoon out of the dish (it can only be done if the spoon is in the dish).
Questions:
With reference to lecture 3, page 20, how many traces of length m there are from a state?
Again with reference to lecture 3, how many Mazurkiewicz's traces (i.e., equivalence classes of traces) there are of length m from a state?
In both cases, you can answer using big-Oh notation as a function of m. Example: rather than 4m2 + 3m - 1 you can answer O(m2). If you find this problem too difficult, you may want to solve it first for n=2, then for n=3.