--- a/Journal/Paper.thy	Mon Dec 17 12:34:24 2012 +0000
+++ b/Journal/Paper.thy	Wed Dec 19 12:51:06 2012 +0000
@@ -1254,6 +1254,70 @@
   for accessing and updating. Apart from having to implement relatively complex data\-structures in C
   using pointers, our experience with the implementation has been very positive: our specification 
   and formalisation of PIP translates smoothly to an efficent implementation in PINTOS. 
+
+  \begin{figure}
+  \begin{lstlisting}
+void lock_acquire (struct lock *lock)
+{ ASSERT (lock != NULL);
+  ASSERT (!intr_context());
+  ASSERT (!lock_held_by_current_thread (lock));
+
+  enum intr_level old_level;
+  old_level = intr_disable();
+  if (lock->value == 0) {
+    heap_insert(thread_preced, &lock->wq, &thread_current()->helem); 
+    thread_current()->waiting = lock;
+    struct thread *pt;
+    pt = lock->holder;
+    while (pt) {
+      heap_update(lock_preced, &pt->held, &lock->helem);
+      if (!(update_cpreced(pt)))
+        break;
+      lock = pt->waiting;
+      if (!lock) {
+        heap_update(higher_cpreced, &ready_heap, &pt->helem);
+        break;
+      };
+      heap_update(thread_preced, &lock->wq, &pt->helem);
+      pt = lock -> holder;
+    };
+    thread_block();
+  } else {
+    lock->value--;
+    lock->holder = thread_current();
+    heap_insert(lock_prec, &thread_current()->held, &lock->helem); 
+  };
+  intr_set_level(old_level);
+}
+  \end{lstlisting}
+  \caption{Our version of the {\tt lock\_release} function (implementing event @{text P}) in 
+  PINTOS.\label{code}}
+  \end{figure}
+
+  Let us illustrate that our specification translates relatively smoothly
+  into C-code. The function {\tt lock\_aquire}, shown in Figure~\ref{code}, 
+  implements the operation that
+  the currently running thread asks for the lock of a specific resource. 
+  In C such a lock is represented as a pointer to the structure {\tt lock}. Lines 2 to 
+  4 contain diagnostic code for PINTOS: first we check that the lock is a ``valid'' lock 
+  by testing it is not {\tt NULL}; second we check that the code is not called
+  as part of an interrupt---aquiring a lock should have been only initiated by a 
+  request from a (user) thread, not an interrupt; third we make sure the 
+  current thread does not ask twice for a lock. These assertions are supposed
+  to be always satisfied because of the assumptions in PINTOS of how this code is called.
+  If not, then there is a bug in PINTOS.
+
+  Line 6 and 7 make the operation of aquiring a lock atomic by disabling all 
+  interrupts, but saving them for resumption at the ond of the function (Line 31).
+  In Line 8, the interesting code of this function starts: we 
+  test whether lock is already taken (its value is 0 for indicating ``already 
+  taken'' and 1 for being ``free''). In case the lock is taken, we need to
+  insert the current thread into the waiting queue of the lock (Line 9,
+  the waiting queue is referenced as @{ML_text "&lock-wq"}). The queues are
+  implemented as Braun Trees providing an heap interface, therefore
+  the function is called @{ML_text "heap_insert"}. Next we
+  record that the current thread is waiting for the lock (Line 10).
+
 *}
 
 section {* Conclusion *}

--- a/Journal/document/root.tex	Mon Dec 17 12:34:24 2012 +0000
+++ b/Journal/document/root.tex	Wed Dec 19 12:51:06 2012 +0000
@@ -9,27 +9,25 @@
 \usepackage{mathpartir}
 \usepackage{tikz}
 \usepackage{pgf}
-%\usetikzlibrary{arrows,automata,decorations,fit,calc}
-%\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}
-%\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf
-%\usetikzlibrary{matrix}
 \usepackage{pdfsetup}
 \usepackage{ot1patch}
 \usepackage{times}
-%%\usepackage{proof}
-%%\usepackage{mathabx}
 \usepackage{stmaryrd}
 \usepackage{url}
 \usepackage{color}
-%%%\titlerunning{Proving the Priority Inheritance Protocol Correct}
-
+\usepackage{courier}
+\usepackage{listings}
+\lstset{language=C,
+        numbers=left,
+        basicstyle=\small\ttfamily,
+        numberstyle=\footnotesize, frame=tb}
 
 \urlstyle{rm}
 \isabellestyle{it}
 \renewcommand{\isastyleminor}{\it}%
 \renewcommand{\isastyle}{\normalsize\it}%
 
-
+%%%\titlerunning{Proving the Priority Inheritance Protocol Correct}
 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
 \renewcommand{\isasymequiv}{$\dn$}
 \renewcommand{\isasymemptyset}{$\varnothing$}

Binary file journal.pdf has changed