Homework 5 due 1-3 December

This is an individualized homework: each student will get a different topic. The homework is to study a topic (reading will be provided via ICON) and prepare a five-slide presentation. Here is the list of topics that will likely be used to assign to students:

  1. Message-based Minimum Spanning Tree Algorithm (the "GHS" algorithm).
  2. Message-based Mutual Exclusion: Lamport Algorithm.
  3. Message-based Mutual Exclusion: Ricart-Agrawala Algorithm.
  4. Message-based Mutual Exclusion: Singhal Algorithm.
  5. Message-based Mutual Exclusion: Maekawa Algorithm.
  6. Message-based Mutual Exclusion: Agarwal and El Abbadi Algorithm.
  7. Message-based Mutual Exclusion: Suzuki and Kasami Algorithm.
  8. Message-based Mutual Exclusion: Raymond Algorithm.
  9. Message-based Load Balancing.
  10. Simulation of Synchrony: the Synchronizer Algorithms.
  11. Decentralized Work-Stealing (?)
  12. Self-Stabilizing Maximal Matching Algorithm.
  13. Message-based Leader Election: Synchronous Ring Topology.
  14. Message-based Leader Election: Asynchronous Ring Topology.
  15. Message-based Termination Detection Algorithm.

(This list is subject to change.) In each case, there is a standard format to the five slides.

Slides could be prepared in many ways: PowerPoint, KeyNote, Prezi, !LaTeX. However, to make things fool-proof for timely display in class, convert the slides to PDF. Avoid black or dark backgrounds.

Homework 4 due 17 November in ICON Dropbox

Write a PlusCal program for four-process consensus, using just two test-and-set shared variables, as described in Homework4.pdf. Translate your program into TLA and run the TLA Simulation to validate that in different executions of the program, all four processes can determine the outcome of the consensus. Probably the best way to do this is to use print statements when a process finishes the consensus code, displaying the value it gets. The simulation output will show searching through all possible executions. Another point you may wish to show is that in any execution, the value returned by all four processes must be the same (thus validating the agreement property of consensus).

Pay attention to step atomicity in your program. In PlusCal, steps are determined by the placement of labels on statements. No step should do more than read or write a single shared variable, except for the test-and-set operation.

When finished, submit your PlusCal program, the associated tla and cfg files, and put comments in your program that explain how its output demonstrates the objectives of the assignment.

Addendum added 15 November In response to questions by two students, here is an attempt to clarify (and maybe simplify) the homework: Homework4Addendum.pdf If this is still unclear, please email and further clarifications can be added.

Homework 3 due 27 October in ICON Dropbox

This is a more challenging and open-ended homework. The problem is to write a PlusCal program that simulates an N-valued shared register, based on using only registers that are 2-valued (binary). The algorithm to use for this is described in unaryreg.pdf. Study that algorithm and also study examples of PlusCal (including ones with Assert statements). There are three main aspects to this assignment.

  1. How to encode the simulation algorithm for Write and Read using PlusCal, which can be compiled into working TLA, then tested using the TLC simulator. The PlusCal page has pcalxlate.jar attached to it, so you can follow the instructions there to translate your code into TLA.

  2. How to test the TLA produced by the previous step. Look again at the TLA Simulation page, which has tlc.jar attached and explains how to use TLC. For testing, you'll need to have small values for any constants in your code. The examples also show invariants, but these won't be so important if you use Assert and Print statements in your PlusCal code.

  3. Once you have the mechanics of writing PlusCal and testing using TLA Simulation, the challenge is to run some experiments and tests that give some confidence that the algorithm behaves correctly under concurrency. Most likely, you will want to try different test cases (using different constants). One question is, how large can N be so that the TLA Simulation runs within a few minutes? Another kind of test is to arrange for multiple "write" and "read" events (at a high layer) to run concurrently: it might be best to have the simulated Write and Read operations be procedures which are called a few times. With these kinds of tests, the program should use Assert and Print statements so that you can see how higher layer invocations and responses are working. You may need to add some additional control variables to control the timing/sequencing of when the higher layer invocations occur (remember that PlusCal has an await statement).

  4. Here's a page with an example, TestAndSet Mutex in TLA, which shows how to convert pseudocode for a mutual exclusion algorithm into PlusCal, and then convert that into TLA and simulate it. It might help to look at that in conjunction with reference to the c-syntax manual for PlusCal.

What to Submit

Ideal would be a short report (perhaps a page, ASCII preferred so that I don't have to convert many different kinds of document like docx, rtf, pdf, ps into something readable) which talks about what experiments were done and why they are some evidence that the Write and Read behave correctly under concurrency. So I will know this report is grounded in technical work, the actual PlusCal code (which may be repeated in different versions for the different experiments) should also be submitted.

The report, supporting programs, and config files can all be put into one directory, compressed into a zip file, then that zip file can be put into the dropbox.

Remarks on Grading/Scoring

[4 Nov 2015] - Several aspects of the submitted work were separately considered for evaluation/scoring. Was there a separate report describing the experiments? Did the report say how the experiments were related to linearizability of the register protocol? If the experiments included timing, did the report offer an explanation of why times grew according to certain parameters? For evaluation of the PlusCal code, an attempt to run the tla file (using the supplied cfg file) was tried, also looking at comments and optional statements in the code (print and assert). In cases where the program didn't run, the logic was inspected to see whether or not the program was a reasonable adaptation of the protocol to PlusCal, hopefully being close to running. For a reasonable adaptation (even if not running), a 75 point score was given; for running code and minimal experiments, 85 points were given. More experiments and more complete descriptions of the experiments got higher scores.

Homework 2 due 22 September in ICON Dropbox

We look once again at the Stadium Wave, this time trying to find some invariants. For this assignment, you don't need to use strict TLA, but you need to be somewhat precise on how you write invariants so there won't be confusion when the homework is evaluated. For the homework, the problem is to find (hopefully strong) invariants about the behavior of processes when the initial configuration can have random states. For example, if we use 0, 1, 2 instead of strings like "Bank", "Fruit Juice", "Camera Brand", then the state of any place in the row can be a random number in {0,1,2}. The challenge is to find some interesting property, described by an invariant, for this behavior.


Homework 1 due 15 September in ICON Dropbox

This homework will be due at the end of the day on Tuesday 15 September (you can still ask questions in class on 15 September).

The homework is to submit a text file, in ASCII (no word-processing files like rtf, doc, or docx, also no pdf files). The text file should contains a TLA+ specification of the behavior of a row of participants in the "Stadium Wave" example. See the stadium.pdf file on the Lectures page for an English description of the behavior.


Homework (last edited 2015-11-20 23:13:50 by Ted Herman)