Specifying and Proving Properties of Guardians for Distributed Systems
In a distributed system where many processors are connected by a networ and communicate using message passing, many users can be allowed to access the same facilities. A public utility is usually an expensive or limited resource whose use has to be regulated. A GUARDIAN is an abstraction that...
| Main Authors: | , , |
|---|---|
| Language: | en_US |
| Published: |
2004
|
| Online Access: | http://hdl.handle.net/1721.1/6313 |
| _version_ | 1811093690986266624 |
|---|---|
| author | Hewitt, Carl Attardi, Giuseppe Lieberman, Henry |
| author_facet | Hewitt, Carl Attardi, Giuseppe Lieberman, Henry |
| author_sort | Hewitt, Carl |
| collection | MIT |
| description | In a distributed system where many processors are connected by a networ and communicate using message passing, many users can be allowed to access the same facilities. A public utility is usually an expensive or limited resource whose use has to be regulated. A GUARDIAN is an abstraction that can be used to regulate the use of resources by scheduling their access, providing protection, and implementing recovery from hardware failures. We present a language construct called a PRIMITIVE SERIALIZER which can be used to express efficient implementations of guardians in a modular fashion. We have developed a proof methodology for proving strong properties of network utilities e.g. the utility is guaranteed to respond to each request which it is sent. This proof methodology is illustrated by proving properties of a guardian which manages two hardcopy printing devices. |
| first_indexed | 2024-09-23T15:49:10Z |
| id | mit-1721.1/6313 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T15:49:10Z |
| publishDate | 2004 |
| record_format | dspace |
| spelling | mit-1721.1/63132019-04-10T18:32:04Z Specifying and Proving Properties of Guardians for Distributed Systems Hewitt, Carl Attardi, Giuseppe Lieberman, Henry In a distributed system where many processors are connected by a networ and communicate using message passing, many users can be allowed to access the same facilities. A public utility is usually an expensive or limited resource whose use has to be regulated. A GUARDIAN is an abstraction that can be used to regulate the use of resources by scheduling their access, providing protection, and implementing recovery from hardware failures. We present a language construct called a PRIMITIVE SERIALIZER which can be used to express efficient implementations of guardians in a modular fashion. We have developed a proof methodology for proving strong properties of network utilities e.g. the utility is guaranteed to respond to each request which it is sent. This proof methodology is illustrated by proving properties of a guardian which manages two hardcopy printing devices. 2004-10-04T14:50:34Z 2004-10-04T14:50:34Z 1979-06-01 AIM-505 http://hdl.handle.net/1721.1/6313 en_US AIM-505 13845108 bytes 10093037 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | Hewitt, Carl Attardi, Giuseppe Lieberman, Henry Specifying and Proving Properties of Guardians for Distributed Systems |
| title | Specifying and Proving Properties of Guardians for Distributed Systems |
| title_full | Specifying and Proving Properties of Guardians for Distributed Systems |
| title_fullStr | Specifying and Proving Properties of Guardians for Distributed Systems |
| title_full_unstemmed | Specifying and Proving Properties of Guardians for Distributed Systems |
| title_short | Specifying and Proving Properties of Guardians for Distributed Systems |
| title_sort | specifying and proving properties of guardians for distributed systems |
| url | http://hdl.handle.net/1721.1/6313 |
| work_keys_str_mv | AT hewittcarl specifyingandprovingpropertiesofguardiansfordistributedsystems AT attardigiuseppe specifyingandprovingpropertiesofguardiansfordistributedsystems AT liebermanhenry specifyingandprovingpropertiesofguardiansfordistributedsystems |