Incremental Proof of the Producer/Consumer Property for the PCI Protocol
Identifieur interne : 001C30 ( Istex/Checkpoint ); précédent : 001C29; suivant : 001C31Incremental Proof of the Producer/Consumer Property for the PCI Protocol
Auteurs : Dominique Cansell [France] ; Ganesh Gopalakrishnan [États-Unis] ; Mike Jones [États-Unis] ; Dominique Méry [France] ; Airy Weinzoepflen [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: We present an incremental proof of the producer/consumer property for the PCI protocol. In the incremental proof, a corrected model of the multi-bus PCI 2.1 protocol is shown to be a refinement of the producer/consumer property. Multi-bus PCI must be corrected because the original PCI specification violates the producer/consumer property. The final model of PCI includes transaction types and reordering along with the completion mechanism for delayed PCI transactions. Verification results include multiple concurrent sessions of the producer/consumer property in a family of topologically isomorphic network configurations. The remaining configurations are identified and left for future work. In contrast to previous case studies involving this problem [13],[15], the incremental proof provides structure which simplifies otherwise difficult monolithic proof attempts.
Url:
DOI: 10.1007/3-540-45648-1_2
Affiliations:
- France, États-Unis
- Grand Est, Lorraine (région), Utah
- Nancy
- Centre national de la recherche scientifique, Institut national de recherche en informatique et en automatique, Laboratoire lorrain de recherche en informatique et ses applications, Mosel (Loria), Université de Lorraine
Links toward previous steps (curation, corpus...)
Links to Exploration step
ISTEX:E621210A3538DB1E250A1A09F796F0A4511A6421Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Incremental Proof of the Producer/Consumer Property for the PCI Protocol</title>
<author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
<affiliation><country>France</country>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
<author><name sortKey="Gopalakrishnan, Ganesh" sort="Gopalakrishnan, Ganesh" uniqKey="Gopalakrishnan G" first="Ganesh" last="Gopalakrishnan">Ganesh Gopalakrishnan</name>
</author>
<author><name sortKey="Jones, Mike" sort="Jones, Mike" uniqKey="Jones M" first="Mike" last="Jones">Mike Jones</name>
</author>
<author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name>
<affiliation><country>France</country>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
<author><name sortKey="Weinzoepflen, Airy" sort="Weinzoepflen, Airy" uniqKey="Weinzoepflen A" first="Airy" last="Weinzoepflen">Airy Weinzoepflen</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">ISTEX</idno>
<idno type="RBID">ISTEX:E621210A3538DB1E250A1A09F796F0A4511A6421</idno>
<date when="2002" year="2002">2002</date>
<idno type="doi">10.1007/3-540-45648-1_2</idno>
<idno type="url">https://api.istex.fr/ark:/67375/HCB-VVP7FG8X-1/fulltext.pdf</idno>
<idno type="wicri:Area/Istex/Corpus">003726</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003726</idno>
<idno type="wicri:Area/Istex/Curation">003683</idno>
<idno type="wicri:Area/Istex/Checkpoint">001C30</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001C30</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Incremental Proof of the Producer/Consumer Property for the PCI Protocol</title>
<author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA, Nancy</wicri:regionArea>
<placeName><region type="region">Grand Est</region>
<region type="old region">Lorraine (région)</region>
<settlement type="city">Nancy</settlement>
</placeName>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
<author><name sortKey="Gopalakrishnan, Ganesh" sort="Gopalakrishnan, Ganesh" uniqKey="Gopalakrishnan G" first="Ganesh" last="Gopalakrishnan">Ganesh Gopalakrishnan</name>
<affiliation wicri:level="2"><country xml:lang="fr">États-Unis</country>
<wicri:regionArea>University of Utah, Salt Lake City, Utah</wicri:regionArea>
<placeName><region type="state">Utah</region>
</placeName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">États-Unis</country>
</affiliation>
</author>
<author><name sortKey="Jones, Mike" sort="Jones, Mike" uniqKey="Jones M" first="Mike" last="Jones">Mike Jones</name>
<affiliation wicri:level="2"><country xml:lang="fr">États-Unis</country>
<wicri:regionArea>presently at Brigham Young University, Provo, Utah</wicri:regionArea>
<placeName><region type="state">Utah</region>
</placeName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">États-Unis</country>
</affiliation>
</author>
<author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA, Nancy</wicri:regionArea>
<placeName><region type="region">Grand Est</region>
<region type="old region">Lorraine (région)</region>
<settlement type="city">Nancy</settlement>
</placeName>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
<author><name sortKey="Weinzoepflen, Airy" sort="Weinzoepflen, Airy" uniqKey="Weinzoepflen A" first="Airy" last="Weinzoepflen">Airy Weinzoepflen</name>
<affiliation wicri:level="3"><country xml:lang="fr">France</country>
<wicri:regionArea>LORIA, Nancy</wicri:regionArea>
<placeName><region type="region">Grand Est</region>
<region type="old region">Lorraine (région)</region>
<settlement type="city">Nancy</settlement>
</placeName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">France</country>
</affiliation>
</author>
</analytic>
<monogr></monogr>
<series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title>
<idno type="ISSN">0302-9743</idno>
<idno type="ISSN">0302-9743</idno>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass></textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Abstract: We present an incremental proof of the producer/consumer property for the PCI protocol. In the incremental proof, a corrected model of the multi-bus PCI 2.1 protocol is shown to be a refinement of the producer/consumer property. Multi-bus PCI must be corrected because the original PCI specification violates the producer/consumer property. The final model of PCI includes transaction types and reordering along with the completion mechanism for delayed PCI transactions. Verification results include multiple concurrent sessions of the producer/consumer property in a family of topologically isomorphic network configurations. The remaining configurations are identified and left for future work. In contrast to previous case studies involving this problem [13],[15], the incremental proof provides structure which simplifies otherwise difficult monolithic proof attempts.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
<li>États-Unis</li>
</country>
<region><li>Grand Est</li>
<li>Lorraine (région)</li>
<li>Utah</li>
</region>
<settlement><li>Nancy</li>
</settlement>
<orgName><li>Centre national de la recherche scientifique</li>
<li>Institut national de recherche en informatique et en automatique</li>
<li>Laboratoire lorrain de recherche en informatique et ses applications</li>
<li>Mosel (Loria)</li>
<li>Université de Lorraine</li>
</orgName>
</list>
<tree><country name="France"><region name="Grand Est"><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
</region>
<name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
<name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name>
<name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name>
<name sortKey="Weinzoepflen, Airy" sort="Weinzoepflen, Airy" uniqKey="Weinzoepflen A" first="Airy" last="Weinzoepflen">Airy Weinzoepflen</name>
<name sortKey="Weinzoepflen, Airy" sort="Weinzoepflen, Airy" uniqKey="Weinzoepflen A" first="Airy" last="Weinzoepflen">Airy Weinzoepflen</name>
</country>
<country name="États-Unis"><region name="Utah"><name sortKey="Gopalakrishnan, Ganesh" sort="Gopalakrishnan, Ganesh" uniqKey="Gopalakrishnan G" first="Ganesh" last="Gopalakrishnan">Ganesh Gopalakrishnan</name>
</region>
<name sortKey="Gopalakrishnan, Ganesh" sort="Gopalakrishnan, Ganesh" uniqKey="Gopalakrishnan G" first="Ganesh" last="Gopalakrishnan">Ganesh Gopalakrishnan</name>
<name sortKey="Jones, Mike" sort="Jones, Mike" uniqKey="Jones M" first="Mike" last="Jones">Mike Jones</name>
<name sortKey="Jones, Mike" sort="Jones, Mike" uniqKey="Jones M" first="Mike" last="Jones">Mike Jones</name>
</country>
</tree>
</affiliations>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Checkpoint
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 001C30 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Checkpoint/biblio.hfd -nk 001C30 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Lorraine |area= InforLorV4 |flux= Istex |étape= Checkpoint |type= RBID |clé= ISTEX:E621210A3538DB1E250A1A09F796F0A4511A6421 |texte= Incremental Proof of the Producer/Consumer Property for the PCI Protocol }}
This area was generated with Dilib version V0.6.33. |