draf.txt
author zhangx
Wed, 27 Jan 2016 23:34:23 +0800
changeset 84 cfd644dfc3b4
parent 81 c495eb16beb6
permissions -rw-r--r--
The parallel of Implementation.thy, i.e. ExtGG.thy has been updated. And some errors in CpsG.thy have also been corrected.

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.