draf.txt
author zhangx
Wed, 03 Feb 2016 21:41:42 +0800
changeset 103 d5e9653fbf19
parent 81 c495eb16beb6
permissions -rw-r--r--
PIPBasics.thy reorganized into sections. The structure is now stable. Next step is to put in more comments.

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.