draf.txt
author zhangx
Wed, 03 Feb 2016 21:05:15 +0800
changeset 102 3a801bbd2687
parent 81 c495eb16beb6
permissions -rw-r--r--
Reorganizing PIPBasics.thy and making small changes to Implementation.thy and Correctness.thy.

There are low priority threads, 
which do not hold any resources, 
such thread will not block th. 
Theorem 3 does not exclude such threads.

There are resources, which are not held by any low prioirty threads,
such resources can not cause blockage of th neither. And similiary, 
theorem 6 does not exlude them.

Our one bound excudle them by using a different formaulation.