News
Project 01 Released. Deadline 14.01.2025, 23:59.
Written on 26.12.2024 16:12 by Andrea Lattuada
Dear Students, I have released the handout for the distributed lock server project. The project is due at 23:59 on Tuesday 14.01.2025. I will not be running the auto-grader on the project, as there is no automatic feedback in addition to successful verification. Read the handout carefully, and refer to the last part of the lecture of December 20th: both contain information on what is expected of you for the project, and how it will be graded (remember that a passing score is required for admission to the exam, and the score for this project will account for 25% of how your performance in the course will be graded).
The project will be scored according to the following criteria:
- Adherence to the English-language specification of the state, steps, and safety property;
- Understandability of the state machine state and steps (prefer enum/structs; use comments where necessary, but not in excess!);
- Identification of inductive invariants, and completeness of the safety proof.
You will not get a passing score for the project if you just submit the handout file unchanged (even if it verifies). You will get a higher score if you submit a project that does not verify but has correct, well-written transitions, an accurate and concise safety property, and at least an attempt to identify the inductive invariant and to write the safety proof. A proof that works for only some of the cases (e.g. some of the host steps) is better than an empty proof, or no invariant.
If you have any questions please reach out. As you work through the project, I strongly recommend you frequently submit your partial work, as that will allow me to give guidance or spot potential common misunderstanding earlier rather than later. I will only evaluate the last submission.