6752 16s1 guest lectures

for everything else about this course go to Rob's page for the course.

Notes/Slides for week 4

Homework for week 4

due April 4th, 4pm, by email to Kai.

Exercise 1

  1. Research the dining philosophers problem.
  2. Model 5 dining philosophers as an abstract machine. Ignore forks for now.
  3. Argue informally that your first model is accurate.
  4. Refine your model to one with forks that are picked up individually.
  5. Show that the model with forks has deadlocks (finite sequences that aren't derivations). These mean that some philosopher starves and that ought to be avoided.
  6. Use the notion of simulation\({}^*\) introduced in the Thursday lecture and prove that your second model simulates the first while preserving who is eating and who is thinking.
  7. Improve your model to prevent deadlocks (and show that the improved model has this property)
  8. Prove that your third model simulates the second one, this time preserving also who has which fork(s).
\({}^*\)For \(i\in\{1,2\}\), let \(M_i = (S_i,I_i,\to_i)\) be an abstract machine with set of initial configurations \(I_i\) satisfying \(I_i\subseteq S_i\). Let \(R\subseteq S_2\times S_1\). We say that \(M_2\) simulates \(M_1\) whenever: Many variations of this notion exist. Sometimes we allow \(M_2\) to have steps that don't match any steps of \(M_1\) but could be matched by an idling step (a self-loop). This has other pitfalls, but again, these can be prevented. One of these is that we could now map every step of \(M_2\) to an idling step. One of the common remedies is to declare parts of the configuration (e.g., certain variables present in the state spaces at both levels) as observable and require that observables are preserved by \(R\). Then, if a step in \(\to_2\) affects the observables, then it cannot be matched by an idling step in \(M_1\).

Exercise 2

  1. Prove that Dekker's critical section algorithm satisfies mutual exclusion (cf. pages 12/13 of slides 1).
  2. Discuss whether you could prove a property called eventual entry, namely that whenever either of the two processes indicates its intent to enter the critical section by setting its intent variable to 1, then eventually (in the temporal logic sense) it will enter its critical section.

Solutions

are here.

Questions?

For reasons of fairness I prefer to not answer assessment related questions via emails. If you have any questions concerning my lectures or these exercises, please use the little Q&A forum I've set up for this purpose. Use common sense for exercise-related questions to avoid spoilers.

Notes/Slides for week 5

Homework for week 5

due April 11th, 4pm, by email to Kai. Apologies for the short notice. I tried to source questions that have reasonably short answers yet are sufficiently challenging and reinforce concepts related to SOS.
  1. Two process graphs, given as states in a labelled transition system, are isomorphic if they only differ in the identity of the nodes. Here is a formal definition. Given a CCS expression \(P\), one can use the denotational semantics given in the notes to give the meaning of \(P\) as a process graph, or we can distill a process graph from the LTS generated by the CCS SOS, namely by taking all states and transitions reachable from \(P\). It is a theorem that those two graphs, both representing the meaning of \(P\), are always bisimulation equivalent.

    Give a counterexample, showing that they are not always isomorphic.

  2. Give an example of TSS that is almost in GSOS format, but fails the requirement that all variables occurring in the source of a rule must be different. Show that bisimulation fails to be a congruence for this TSS.
  3. Here is an operational semantics of the sequencing operator: \[ \frac{x\stackrel{a}{\longrightarrow}x'}{x;y\stackrel{a}{\longrightarrow}x';y}~\text{for }x' \neq 0 \qquad\qquad \frac{x\stackrel{a}{\longrightarrow}0}{x;y\stackrel{a}{\longrightarrow}y} \] Is it in GSOS format? What is wrong with this operational semantics? Show that strong bisimulation is not a congruence for this operator (in the context of CCS).
  4. Give a structural operational semantics in GSOS format of the sequencing operator.

Maintained by: Kai Engelhardt
Last modified: Mon Apr 4 16:40:47 AEST 2016