Formal Verification of Systems Software

Dear Students, you should have received emails with your results for Project 2. The score is out of 20 points: 10 points is the minimum score to pass.

Additionally, in "Materials" you can find the Appendix that will be part of your handout at the exam. I may still add material to the appendix: if that happens, I will let you know.
No other written aids will be allowed at the exam. You can refer to the last lecture for an overview of the kinds of problems that may be part of the exam.

For Project 2, the maximum scores for each graded section are as follows (your score for each is in [[x]] in the feedback)

high level spec:    
put    1
get    1
noop    1
    
host:    
init    1
get    1
put    1
send    2
recv    2
    
refinement proof:    
interpretation functions    1
invariant    2
    
refinement_init proof    2
refinement_next proof    5

Dear Students, if you are an Erasmus or freemover exchange student that cannot register for the exam through HISPOS you should have just received an email from me with further instructions. If you are one such student and have not received a direct email about exam registration, you need to reach out by the end of this week to ensure you are properly registered for the exam.

Additionally, a number of students who would be admitted to the exam based on the homework exercises and Project 1 have not yet registered on HISPOS: I recommend you do so now. Once I publish the result of Project 2 (at the end of this week), I will inform any student who is registered but no longer fulfills the exam admission requirements, so you can de-register by the deadline.

Dear Students, please note that the proof function `noop_preserves_spec_view` uses the term `noop` to indicate that the distributed system state does not change, and this use of the term is unrelated to a `NoOp` step. This is also indicated by the function's pre- and post-conditions and by the comment on the function.

In the meantime, you should have received emails with your results on Project 1. The score is out of 20 points: 10 points is the minimum score to pass. Everyone who's submitted has passed, well done! The maximum scores for each graded sections are as follows (your score for each is in [[x]] in the feedback):

host transitions:
    init: 2
    grant: 3
    receive: 3
safety property: 3
safety proof:
    invariants: 4
    init_implies_inv proof: 1
    inv_inductive proof: 4
 

Dear Students, we will be releasing the scores for Project 1 soon (we are currently double-checking the scores). One common mistake that I found across a number of submissions is including the enabling condition that a host does not have the lock in the transition that accepts a grant message (and thus lets that host acquire the lock): this enabling condition (often expressed something like `&&& !s1.has_lock` was not mentioned in the English-language specification, and it's a property that could (and likely should) be part of the invariant (or implied by the invariant), but does not belong in the step, as it's implied by the admissible behaviors, but it's not part of the protocol design per-se.

As this information might be helpful for Project 2 and because we have canceled the Chapter 8 exercise, we will extend the Project 2 deadline till Thursday February 6th at 23:59.

Dear Students, today we'll cover some advanced topics and we'll let you try them out in class, so if you can, please bring a laptop with you (I realize this is very last minute, for which I apologize, we'll have an alternative for those of you that don't have a laptop with you). You'll be able to find the handouts for today under "Materials" in the next few minutes.

Dear Students, I have opened a new registration for office hours from Project 02: please register if you need to. By default we'll assign times starting at 13:00 tomorrow (January 30th). I'll email you with a slot when you register, and you can let me know if it doesn't work for you, and we'll find another time.

Dear Students, I was made aware that there is a stray paragraph in the handout for Project 2, in the section on proof tooling. This paragraph escaped my proof reading, but should have been removed.

The following paragraph does not apply to the Verus version of the course (the one you're taking) and you can safely ignore it:

Dafny's internal map axioms can get pretty timeout-y in this situation. The second thing this gift provides is some judicious automation control: some {:opaque}d boundaries and "accessor" lemmas you can use to interact with the {:opaque}d definitions without revealing them in your own proofs. You don't need to reveal anything we've opaqued here, nor do you want to, so you can avoid timeouts traps.

My apologies for the oversight.

Dear Students, don't forget that you need to pass 7 out of 8 chapters of exercises to be admitted to the exam, and note that Chapter 7 is due soon, on January 28th. If you haven't started on it, note that submitting a compliant exercise is sufficient to pass, even if it doesn't verify. This is also a reminder that the tutorial this week is canceled, and registration for office hours for project 2 are open: please register for them under "registrations" (we can accommodate times other than the tutorial session). Do not wait until the last minute, as I cannot guarantee that I'll be able to provide office hours slots next week.

Dear Students, there won't be a regular tutorial this week (on January 29th). You can register for office hours for Project 2 in "Registrations". By default you'll be assigned a slot during the tutorial time on Wednesday (which is otherwise canceled). You can attend either in person (in my office, E 1 5, 448) or on Zoom (meeting details sent separately). Make sure you have submitted the current version of your project code before registering for office hours - once you register you'll receive an individual email with a time assignment.

Dear Students, if you have questions regarding Project 2, please compile them in a txt or pdf file and submit them by tomorrow January 23rd at 18:00 via the "Project 02: Sharded Key-Value Store" submissions. Please keep these as short as possible, and note there won't be individual answers to these, but I will go over them and discuss them on Friday (to the extent possible). And, as mentioned before, if you need individual help, please register for office hours under "Registrations": I will only accept registrations for office hours from students who have submitted the current version of their attempt to the "Project 02" submission.

Dear Students, there will not be a tutorial on Wednesday (January 22nd) this week.

If you need help with the project, I will be offering office hours sessions between the end of this week and beginning of next week. Please register your interest in the "Registration" that I opened ("Project 02 - Office Hours - 01").

Dear Students, don't forget that you need to pass 7 out of 8 chapters of exercises to be admitted to the exam, and note that Chapter 6 is due soon, on January 21st. If you haven't started on it, note that solving exercise01 is sufficient to pass, which should be fairly straightforward. I recommend not waiting till the last day to submit, as usual, in case there are issues with your submission.

Dear Students, as mentioned in class, tomorrow we will release the handout for Chapter 07. The submission is due on January 28th.
A few notes:

• Like for chapter 5, submitting a compliant file (even if it doesn’t verify) grants you a point
• If you pass the auto-grader (no hidden checks, just compliance and successful verification), you get an additional point
• You need 1 out of 2 points needed to pass
  • I still strongly recommend attempting the exercise, as there may be questions about the refinement to an implementation in the exam
  • but you should prioritize Project 2.
• If you score 2 points, you get a 8% bonus on the overall score of the projects + exam
  (relative to the maximum 100% score, not your score)
  ​​​​​This does not affect or change the requirement to pass the exercises and projects to be admitted to the exam
• I reserve the right to add additional constraints and invalidate the bonus if a solution trivializes the verification in a way that I did not guard against (i.e. you should be faithful to the intent of the exercise -- if you are, then you'll likely get the bonus if you get the exercise to verify successfully)

Dear Students, it came to my knowledge that the new version of Verus that was published last week did not work with older versions of glibc (ie a number of slightly older Linux distributions were affected). I published a new version that should restore the same level of support as before. If you’re on Linux, and you have had issues with the new Verus version, you can download the new version (from the Verus setup page on CMS). If the version you’re using works for you, you don’t need to do anything. There should be no change in which code verifies between the two versions. My apologies for the inconvenience if you were affected.

Dear Students, if you want to discuss Project 1 in an office-hours setting, please register for it using the "Registration" in CMS that I just opened (and that remains open until tomorrow evening). Based on registrations there I will schedule office-hours meetings on Friday January 10th and Monday January 13th.

Dear all, I would like to make a small clarification to the English-language description in the handout of Project 1.
Specifically, you should read the fourth paragraph as follows (it is unchanged, except for the part added in bold):

To guard against duplicate messages, the nodes associate a monotonically increasing epoch number with the lock. Initially, node 0 (if present) holds the lock and its epoch number is 1, while all other nodes with an epoch of 0 (and not holding the lock). A node that holds the lock can “grant” it to another node by sending them a “Grant” message which has an epoch number that is greater than the node's epoch number. A node that receives such a message will become the new holder and will set its epoch number to the message’s epoch number. A node should reject (i.e. not receive) lock "Grant" messages with epochs lower or equal to their current epoch, as these are stale (duplicates).

---

Additionally, please note that I believe it is very unlikely that a safety property that is expressed concisely will also be inductive by itself for this protocol. If you did not need any additional conjuncts in your `inv` in addition to `safe` I would strongly recommend carefully inspecting your protocol definition and safety property.

All of this will also be discussed during the tutorial tomorrow.

Dear Students, if you need help with one of the exercises, or have questions regarding the project, please send me an email (andrea@mpi-sws.org) to book a time between 11:00 and 16:30 today. I will acknowledge the time (if available, or suggest a different time) and then we will meet in this Zoom room:

https://eu02web.zoom-x.de/j/61362418777?pwd=L6hG2gnXZIyaiZbuE26MKQEbnrOhL9.1
Meeting ID: 613 6241 8777
Passcode: 581423

If you've already sent me an email, you will get a response in the next hour or so.

Please also let me know if you need help but today does not work for you.

Dear Students, just a quick note that I have made available the individual feedback for Chapter 4 for students that submitted by December 20th. Please make sure to download it by Friday January 3rd, as I will start running the auto-grader again on Saturday January 4th, which (due to a limitation in how the feedback is uploaded and updated) will overwrite the manual feedback. If you are unable to download the feedback by then, you will be able to request it directly via mail from me afterwards.

Dear Students, apologies for a second email in one day.

The first few submissions for project 01 have made me notice that, while the project file is correct, it allows for certain kinds of unfortunate typos that may make your proof meaningless. I cannot guard against the majority of them, obviously (you are in charge of being careful in writing your specification and safety property, as we discussed at length), but in an attempt to better evaluate your skills in the project I have added a pseudo_liveness proof obligation (akin to the ones you have seen before in exercises) for exercise01.rs that will hopefully help you catch certain careless mistakes.

If you have already submitted, I have applied the patch to your code and re-submitted for you: you can download the updated code from your personal status page. If you have not submitted you have two options:

(a) recommended, especially if you've only done a little bit of work: re-download the handout and copy over your solution within the grading markers,

(b) use the write up at https://cms.sic.saarland/sysverification2425/contents/view/6 to apply the change to exercise01.rs (note that you will need to do this carefully, to make sure that your code will pass the auto-grader check for changes outside the grading markers)

Sorry for the inconvenience, and hope this helps.

Dear Students, one quick clarification. As for all the other exercises you are still only allowed to change code within the /*{*/ and /*}*/ markers. To let you check that your code is compliant, contrary to what I had mentioned before, I will be running the auto-grader on the project periodically, so you can get reports in case you accidentally make changes outside the markers. One more reason to submit early, even partial progress.

Dear Students, a quick heads up on how chapter 5 is scored (due to its unusual requirement that the minimum score to pass is 0/1 as long as you do submit `extercise04.rs` to the Chapter 04, 05 submission): in the Tests/Exam view for Chapter 5 you will see that you will receive 1 point if you have submitted `exercise04.rs`, and 2 points if it passes the auto-grader: I have set the pass score on CMS to 1/2 points, which you will get if you have at least submitted `exercise04.rs`. During the non-teaching period I will only update the scores occasionally, so if you have recently submitted chapter 5, it may be that the point(s) have not been awarded yet. Let me know if something is unclear, or if you have any questions.

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.

Dear Students, I have released the handout for chapter 5, which consists of a single file, exercise04.rs, that you can add to the files for chapter 4. Note that it verifies successfully with the trivial definition of safety for the protocol included in the handout for exercise03.rs: this is a meaningless proof, as it is a proof that true is a valid safety property for two-phase commit. Only work on this exercise once you believe you have a sufficiently accurate specification of two-phase commit in exercise03.rs. The passing score for this Chapter 5 is 0/1, assuming you make an attempt and submit: submitting exercise04.rs alongside the Chapter 4 files to the "Chapter 4, Chapter 5" submission is sufficient to pass Chapter 5. The passing score for Chapter 4 remains 2/3 (for exercise01, exercise02, exercise03). While it's not required to pass, I recommend you work on trying to complete the proof, as it's good practice for the project, which will be released soon.

Dear Students, there is a small issue in exercise01.rs in the handout I distributed for Chapter 4 (and Chapter 5). For an accurate model of the system, we need to state that the network's sent_msgs Set is finite as a well_formed condition. This will not have prevented you from proving safety and is a weaker network property (so it's not incorrect, just models a network where the messages could be infinite); but the update is still a valid, and more accurate, network model and makes the proof for Chapter 5 simpler.

If you have already submitted, I have applied the patch to your code and re-submitted for you: you can download the updated code from your personal status page. If you have not submitted you have two options:

(a) recommended, especially if you've only done a little bit of work: re-download the handout and copy over your solution within the grading markers,

(b) use the write up at https://cms.sic.saarland/sysverification2425/5/Chapter_4_Patch to apply the change to exercise01.rs (note that you will need to do this carefully, to make sure that your code will pass the auto-grader check for changes outside the grading markers)

Sorry for the inconvenience.

I will also soon update the incremental.rs example from the last lecture demos to match the same network model.

Dear Students, the handout for chapter 4 has been released. It includes exercise01.rs, exercise02.rs, and exercise03.rs.
You can submit your solution to the Chapter 04, Chapter 05 submission on CMS. We will later release chapter 5, which consists of exercise04.rs. When we do, you can add exercise04.rs alongside the files in this handout (it depends on them), and then resubmit to the Chapter 04, Chapter 05 submission on CMS.

You need 2/3 points to pass Chapter 4. We'll communicate the pass threshold for Chapter 5 when we release it.

While the deadline for both Chapter 4 and Chapter 5 is January 7th 2025, as noted in the lecture: if you submit your solution to Chapter 4 by the end-of-day on December 20th I will give you feedback on it. This feedback can be quite useful for the first graded project, which will be released on December 21st.
 

Dear Students, tomorrow I will be holding a virtual office hours session for the Chapter 3 exercises from 9:00 till 14:00.

You can either walk into my office in E1 5 (SWS) 448, or join the following Zoom meeting:
https://eu02web.zoom-x.de/j/67226483076?pwd=bkto7auPFHecO5uCXUmp9aCHJTzkaQ.1
Meeting ID: 672 2648 3076
Passcode: 000725

There may be a wait, if multiple people join the Zoom meeting or show up at the same time. My apologies in advance.

If you need help and cannot make it to the office hours tomorrow, please email me: andrea@mpi-sws.org

Dear Students, if you've previously submitted questions on chapter 2 exercises, I should have by now either addressed the question during the tutorial or lecture, or have given you a personal answer as "feedback" to the submission: if that's not the case, please submit again.

I have re-opened the "Chapter 02: Basics and Specification - Questions" Submission (you can reach it from your "Personal Status" page, like a regular exercise submissions) for you to submit questions on the Chapter 2 exercises. You can upload a txt, rtf, pdf, Word, or zip file (containing multiple of the file types I listed; if you submit something else I can't guarantee I'll be able to open it): you can only submit one file, so if you have multiple questions, add them all to one file / zip file.

I will run the auto-grader every day from now till the deadline, for you to have more opportunities to test your code against the auto-grader.

If you haven't submitted yet, you should do so by the end of the day today, as you only have four more rounds of feedback until the deadline. If you only have a partial solution, submit anyway, to get at least some feedback from the autograder.

Dear Students, I have re-opened the "Chapter 02: Basics and Specification - Questions" Submission (you can reach it from your "Personal Status" page, like a regular exercise submissions) for you to submit questions on the Chapter 2 exercises. You can upload a txt, rtf, pdf, Word, or zip file (containing multiple of the file types I listed; if you submit something else I can't guarantee I'll be able to open it): you can only submit one file, so if you have multiple questions, add them all to one file / zip file. If you've already submitted,

I have made a copy of all the questions and (hopefully) answered them all during the exercise session yesterday (the recording is available): if you've already submitted and have further questions, feel free to replace your submission with further questions (they're timestamped, so I'll know that you have additional questions, but note that if you then replace the submission again, I'll only see the latest version). If you submit a question, please make sure you have also submitted at least a partial solution to the exercise itself (the "Chapter 02: Basics and Specification" submission), so I can reference your code if needed.

For questions I receive by the end of the day today, I'll give an answer or hint at the start of tomorrow's lecture.

Dear Students, I have opened another Submission (you can reach it from your "Personal Status" page, like a regular exercise submissions) for you to submit questions on the Chapter 2 exercises (it's called "Chapter 02: Basics and Specification - Questions"). You can upload a txt, rtf, pdf, or Word file: you can only submit one file, I believe, so if you have multiple questions, add them all to one file. If you're finding some of the exercises challenging, please let me know through that channel, so I can try and adjust tomorrow's tutorial based on the feedback. Make sure you don't submit questions to the main "Chapter 02: Basics and Specification" submission, as that would score you zero points for Chapter 02, while "Chapter 02: Basics and Specification - Questions" is obviously not graded.

Dear Students, This is a gentle reminder that the Chapter 01 exercises are due on Friday November 22nd at 23:59. A few notes and reminders:

• we provide feedback on the exercises every other day (we'll provide feedback today, Wednesday, and Friday just after the lecture);
• Chapter 00 was just a test exercise and does not count towards the 7 out of 8 exercises you need to pass to have access to the exam;
• if you haven't submitted yet, you haven't missed any deadline yet (the first graded exercise is Chapter 01, open till Friday);
• if you have questions or issues regarding the exercises: please reach out as soon as possible and directly (not via the "feedback" button on CMS, because that anonymizes your comment so I cannot respond -- you're welcome to use the "feedback" button on CMS for any other feedback you want to send anonymously);
• if you believe that the feedback you received is not correct, please reach out immediately (andrea@mpi-sws.org); do not wait until the deadline, as you won't have the chance to re-submit, in case the feedback is in fact correct;
• do not change the exercise filenames, do not add comments to the exercises outside the "editable area" markers (/*{*/ /*}*/)

See you on Wednesday in E1 5 029.

Dear Students, I am currently traveling for a conference and due to a flight delay I will not be able to make it back to Saarbrücken by Friday morning, so the in-person lecture is canceled this week. We will nonetheless release the first set of graded exercises on Friday, and you will have two weeks to complete them. I have already covered the lecture material necessary to complete these exercises but I will record and publish a brief introduction to the exercises with a refresher and some hints. You will also be able to ask questions at the tutorial next week.

See you on Wednesday!

The tutorial today (October 30th) will take place in E1 5 002, the same room as the first two lectures, at 16:10. This is for this week only. We'll move to E1 5 029 for both lectures and tutorials starting next week.

Also note that there (obviously) won't be a lecture this Friday (November 1st), and there won't be a tutorial next week (on Wednesday November 6th). After today's tutorial, the next session will be the lecture on Friday November 8th at 10:15 in E1 5 029.

Here is more info on how to find the rooms.

Dear all, based on the preferences you entered, we've scheduled the tutorial on Wednesdays at 16:10-17:00. The first tutorial will be next week, on October 30th. As a reminder, the tutorials will be recorded, but we strongly recommend in-person attendance, as they will be interactive and give you the opportunity to ask questions about the material, take home exercises, and projects. Thank you all for entering your preferences.