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
Thu, 28 Jan 2016 21:14:17 +0800
changeset 90 ed938e2246b9
parent 81 c495eb16beb6
permissions -rw-r--r--
Retrofiting of: CpsG.thy (the parallel copy of PIPBasics.thy), ExtGG.thy (The paralell copy of Implemenation.thy), PrioG.thy (The paralell copy of Correctness.thy) has completed. The next step is to overwite original copies with the paralell ones.
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