Description

Homework 7: Separation Logic, Nondeterminism, and Parallelism
Prof. Stefan Muller
This assignment contains 8 written task(s) for a total of 66 points.
Logistics
Please read and follow these instructions carefully.
• Submit your written answers in a single PDF or Word document. Typed answers are preferred (You can use any program as long as you can export a .pdf, .doc or .docx; LaTeX is especially good for typesetting logic and math, and well worth the time to learn it), but legible handwritten and scanned answers are acceptable as well.
• Your Blackboard submission should contain only the file with your written answers. Do not compress or put any files in folders.
Read the policy on the website and be sure you understand it.
1 Linked list and separation logic
Task 1.1 (Written, 10 points).
In class, we wrote a program that appends a list of length three to a list of length m. Now, write a program that operates on a list L with a length of m + 3 and starting head variable head. This program should create two lists L1 and L2, where L1 contains the first three elements of L with the head variable head1 and L2 contains the remaining elements of the list L with the head variable head2.
Task 1.2 (Written, 12 points).
Write a precondition and a postcondition for your program in Task 1.1 that specifies its intended behavior. Using a proof outline, prove that your program adheres to the specification. Use the list(L,i,n) predicate in your specifications and the separation logic rules in the proof outline.
Write a full proof outline. You do not, however, need to separately justify the proof obligations (but they must be correct).
2 Resource logic
Task 2.1 (Written, 10 points).
For each resource logic formula, draw one heap (in the style of the diagrams of Figures 1, 2, and 3 of the Lecture 21 notes) that satisfies it.
a) x 7→ x
b) x 7→ 2 ∗ y 7→ 2
c) x 7→ x + 1,x
d) w 7→ 2 ∗ (x 7→ y ∧ y = w)
e) (∃x.y 7→ x) ∧ y 7→ 2
Task 2.2 (Written, 6 points).
For each resource logic formula, draw two heaps that satisfy it.
a) x ,→ x
b) x ,→ 2 ∧ y ,→ 2
c) x 7→−
Task 2.3 (Written, 8 points).
For each implication, either prove it using the axioms and rules of resource logic or provide a counterexample. Specify which rule you are using by referring to its line number in Section 2 of the separation logic lecture.
a) (x 7→ 2 ∗ y 7→ 2) ∗ z 7→ 2 ⇒ (z →7 2 ∗ y →7 2) ∗ x 7→ 2
b) (x ,→ 3 ∧ y ,→ 3) ⇒ x = y
c) emp∗ ((∃x.y 7→ x) ∗ w 7→ 2) ⇒∃x.(y →7 x ∗ w 7→ 2)
d) (∃x.y 7→ x) ∗ x 7→ 2 ⇒∃x.(y 7→ x ∗ x 7→ 2)
3 Nondeterminism
Task 3.1 (Written, 10 points).
a) Using the small step semantics write one (nondeterministic) execution of the program
S1 ≜ while {x ≥ 0 → y := x/y □ x ≤ 0 → y := y ∗ x}
on the state σ ≜{x = 0,y = 1}. If the execution does not terminate, write at least three iterations of the loop.
b) What is M(S,σ)?
4 Parallel programs
Task 4.1 (Written, 10 points).
Consider the program

S2 ≜ [ x := y;y := y + 1 ∥ y := y + 3 ]
and the initial state σ ≜ {x = 3,y = 2} and a heap h. Draw the evaluation graph for this program describing the possible behaviors of S2.
5 One more wrap-up question
Task 5.1 (Written, 0 points).
How long (approximately) did you spend on this homework, in total hours of actual working time? Your honest feedback will help us with future homeworks.