Index: c/preemption
===================================================================
--- doc/preemption	(revision 9ea8a7ca32a0148a8f388e6313b10d79946deda1)
+++ 	(revision )
@@ -1,58 +1,0 @@
-Kernel makes it possible for a thread to be preempted anytime when
-IRQ's are enabled on local CPU. This arrangement triggers a discussion
-about its correctness and efficiency.
-
-The correctness issue relates to the possibility of preempting a
-thread holding a spinlock. It is natural to ask whether such a
-preemption can lead to a deadlock. By proving the following lemma, we
-will show that deadlock is actually not possible.
-
-Lemma:
-  On condition that each spinning lock is always locked on the same
-  CPU priority level (either always with IRQ's disabled or always
-  with IRQ's enabled), otherwise correct code never deadlocks.
-
-Proof:
-  Let all assumptions from the lemma hold.
-  Let us further assume that we have encountered a deadlock.
-  We will analyse all likely ways how that could have happened.
-
-  a)  Deadlock happened between two CPUs. This means that there must
-  have been wrong lock-ordering. Code with lock-ordering problems is
-  considered incorrect and contradicts our assumptions.
-  
-  b)  Deadlock happened between two threads of execution executing on
-  the same CPU. 
-
-  b1) If one thread of execution was servicing an interrupt and the
-  other was executing in thread context, our assumption that each
-  spinning lock is acquired always on the same CPU priority level is
-  violated.
-  
-  b2) The last likely scenario is that the deadlock happened between
-  two threads executing on the same CPU with IRQ's enabled.  Again,
-  this means that we were working with incorrect code because it
-  contained wrong ordering of lock operations.
-  
-  Since there is no possibility left, except for trivial errors, we
-  have shown that the deadlock contradicts with our assumptions and
-  therefore is not possible.
-
-  Q.E.D.
-  
-Notes on the proof:
-  ad a)  Deadlock between two CPUs is independent on the preemption
-         model. If we have this kind of deadlock, we would have had
-	 the same kind of deadlock on an ordinary SMP system with
-	 kernel preemption disabled.
-	 
-	 This preemption model makes UP behave more like SMP because
-	 it introduces some SMP specific specialities.
-
-  ad b2) Notice that the scenario when thread A acquires lock X and
-	 gets preempted in favor of thread B which is trying to
-	 acquire lock X, doesn't deadlock the two threads. Of course,
-	 B won't be allowed to get X until A releases it, but that
-	 will certainly	happen because B too will sooner or later be
-	 preempted. This scenario emphasizes the efficiency issues,
-	 though.