$Id: index.html,v 1.2 2008/09/22 10:55:15 kaie Exp kaie $
Mark distribution
Marks & Deadline
Assignment 1 is worth 16 marks. The deadline is 23:59:59 EST (Sydney
local time), Wednesday September 24 2008.
Introduction
In 2007 I received an email from an old school friend who ended up in
industry developing machines
to check the result of cleaning processes for return bottles (Most
of Germany's beverages are sold in return bottles that are re-used
about 30 times on average.) Here's a partial and half-mechanical
translation. Apologies for the Germish:Hello [...]
on the search for alternatives to Lamport's bakery algorithm I
stumbled coincidentally over your work. [...] some Java processes and
some C processes are coupled over a shared memory region. Since I can't
access atomic operations on the shared memory in java, I'm currently
using Lamport's bakery algorithm to lock the region. I am however
still on the lookout for a better-behaved alternative. Do you know
anything like that?
Best regards to the other end of the world,
(name withheld)
Assignment Specification
This assignment consists of 3 tasks. All of them are related to the
critical section problem and Lamport's bakery algorithm.
Problem Statement
Lamport's bakery algorithm uses potentially unbounded ticket numbers. Develop an improved bakery algorithm that has the same remarkable properties as the original but uses bounded ticket numbers only.
Tasks
Overview
- Write and test your solution using C and pthreads but without
any semaphore or lock operations (these are simply not available on
the target system). Call two functions,
critical(pid,ticket) as the critical section, and
noncritical(pid) as the non-critical section, where the
argument pid is the process ID and ticket is
the ticket number. (See and use critical.h v1.2 and critical.c v1.4.)
- Model your solution in Promela and try to verify its relevant
properties for a small number of processes (more than 2 please).
- Discuss your solution.
- Prove its relevant properties (mutual exclusion, absence of
deadlock, absence of unnecessary delay, eventual entry, which in
this case should be linear waiting).
- Describe the time complexity of the entry and exit protocols
in terms of the overall number of processes and the number of
processes currently wanting to enter the CS.
- Describe the expected number of accesses to shared variables
of the entry and exit protocols in terms of the overall number of
processes and the number of processes currently wanting to enter
the CS.
- Describe exactly how the relevant properties of your Promela
program can be verified by listing options and formulae.
The C programming task requires you to write a program that
takes 2 command line arguments: the number
n of processes and the number
k of iterations of the loop in each process.
Submission
Required files are:
- ibakery.c
- C solution
- ibakery.pml
- Promela solution
- ibakery.tex
- LaTeX document describing your
programs and proofs.
Optional files are:
- ibakery.ltl
- Spin LTL file to accompany your
Promela program
- *.eps
- up to 10 diagrams in Encapsulated PostScript
format are accepted
Note that size limits apply to individual files as well as to the
submission as a whole.
Testing
Your C solution must compile and function on standard CSE lab
machines as well as SMP machines such as weill and
williams.
Your C solution will be tested by running, e.g.,
$ gcc -Wall -Werror -lpthread -o ibakery ibakery.c
$ ibakery 100 10000
Your Promela solution will be tested in xspin.
Your proof will be tested by running something slightly smarter than
$ latex ibakery.tex
$ latex ibakery.tex
$ xdvi ibakery
Submission Instructions
Submission is now enabled. One student per pair should submit using
a command similar to (but maybe listing some optional files):
give cs3151 ass1 ibakery.c ibakery.pml ibakery.tex
$Log: index.html,v $
Revision 1.2 2008/09/22 10:55:15 kaie
*** empty log message ***
Revision 1.1 2008/09/09 09:04:19 kaie
Initial revision
Maintained by: COMP[39]151
Last modified: Thu Nov 20 17:10:30 EST 2008