1257 

  1258   \begin{figure}

  1259   \begin{lstlisting}

  1260 void lock_acquire (struct lock *lock)

  1261 { ASSERT (lock != NULL);

  1262   ASSERT (!intr_context());

  1263   ASSERT (!lock_held_by_current_thread (lock));

  1264 

  1265   enum intr_level old_level;

  1266   old_level = intr_disable();

  1267   if (lock->value == 0) {

  1268     heap_insert(thread_preced, &lock->wq, &thread_current()->helem); 

  1269     thread_current()->waiting = lock;

  1270     struct thread *pt;

  1271     pt = lock->holder;

  1272     while (pt) {

  1273       heap_update(lock_preced, &pt->held, &lock->helem);

  1274       if (!(update_cpreced(pt)))

  1275         break;

  1276       lock = pt->waiting;

  1277       if (!lock) {

  1278         heap_update(higher_cpreced, &ready_heap, &pt->helem);

  1279         break;

  1280       };

  1281       heap_update(thread_preced, &lock->wq, &pt->helem);

  1282       pt = lock -> holder;

  1283     };

  1284     thread_block();

  1285   } else {

  1286     lock->value--;

  1287     lock->holder = thread_current();

  1288     heap_insert(lock_prec, &thread_current()->held, &lock->helem); 

  1289   };

  1290   intr_set_level(old_level);

  1291 }

  1292   \end{lstlisting}

  1293   \caption{Our version of the {\tt lock\_release} function (implementing event @{text P}) in 

  1294   PINTOS.\label{code}}

  1295   \end{figure}

  1296 

  1297   Let us illustrate that our specification translates relatively smoothly

  1298   into C-code. The function {\tt lock\_aquire}, shown in Figure~\ref{code}, 

  1299   implements the operation that

  1300   the currently running thread asks for the lock of a specific resource. 

  1301   In C such a lock is represented as a pointer to the structure {\tt lock}. Lines 2 to 

  1302   4 contain diagnostic code for PINTOS: first we check that the lock is a ``valid'' lock 

  1303   by testing it is not {\tt NULL}; second we check that the code is not called

  1304   as part of an interrupt---aquiring a lock should have been only initiated by a 

  1305   request from a (user) thread, not an interrupt; third we make sure the 

  1306   current thread does not ask twice for a lock. These assertions are supposed

  1307   to be always satisfied because of the assumptions in PINTOS of how this code is called.

  1308   If not, then there is a bug in PINTOS.

  1309 

  1310   Line 6 and 7 make the operation of aquiring a lock atomic by disabling all 

  1311   interrupts, but saving them for resumption at the ond of the function (Line 31).

  1312   In Line 8, the interesting code of this function starts: we 

  1313   test whether lock is already taken (its value is 0 for indicating ``already 

  1314   taken'' and 1 for being ``free''). In case the lock is taken, we need to

  1315   insert the current thread into the waiting queue of the lock (Line 9,

  1316   the waiting queue is referenced as @{ML_text "&lock-wq"}). The queues are

  1317   implemented as Braun Trees providing an heap interface, therefore

  1318   the function is called @{ML_text "heap_insert"}. Next we

  1319   record that the current thread is waiting for the lock (Line 10).

  1320