Mercurial Mercurial > hg > pip / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
81
c495eb16beb6 CpsG.thy restored. It was deleted. But now restored as a temporary holder of PIPBasics.thy.
zhangx
parents:
diff changeset 
     1
 
There are low priority threads,
c495eb16beb6 CpsG.thy restored. It was deleted. But now restored as a temporary holder of PIPBasics.thy.
zhangx
parents:
diff changeset 
     2
 
which do not hold any resources,
c495eb16beb6 CpsG.thy restored. It was deleted. But now restored as a temporary holder of PIPBasics.thy.
zhangx
parents:
diff changeset 
     3
 
such thread will not block th.
c495eb16beb6 CpsG.thy restored. It was deleted. But now restored as a temporary holder of PIPBasics.thy.
zhangx
parents:
diff changeset 
     4
 
Theorem 3 does not exclude such threads.
c495eb16beb6 CpsG.thy restored. It was deleted. But now restored as a temporary holder of PIPBasics.thy.
zhangx
parents:
diff changeset 
     5
 












c495eb16beb6
CpsG.thy restored. It was deleted. But now restored as a temporary holder of PIPBasics.thy.



zhangx


parents: 

diff
changeset




     6


There are resources, which are not held by any low prioirty threads,













c495eb16beb6
CpsG.thy restored. It was deleted. But now restored as a temporary holder of PIPBasics.thy.



zhangx


parents: 

diff
changeset




     7


such resources can not cause blockage of th neither. And similiary, 













c495eb16beb6
CpsG.thy restored. It was deleted. But now restored as a temporary holder of PIPBasics.thy.



zhangx


parents: 

diff
changeset




     8


theorem 6 does not exlude them.













c495eb16beb6
CpsG.thy restored. It was deleted. But now restored as a temporary holder of PIPBasics.thy.



zhangx


parents: 

diff
changeset




     9














c495eb16beb6
CpsG.thy restored. It was deleted. But now restored as a temporary holder of PIPBasics.thy.



zhangx


parents: 

diff
changeset




    10


Our one bound excudle them by using a different formaulation. 













c495eb16beb6
CpsG.thy restored. It was deleted. But now restored as a temporary holder of PIPBasics.thy.



zhangx


parents: 

diff
changeset




    11
















pip