Specifying and Proving Properties of Guardians for Distributed Systems
This report describes research conducted at the Artificial Intelligence Laboratory of the Massachusetts Institute of Technology. Support for the laboratory's artificial intelligence research is provided in part by the Advanced Research Projects Agency of the Department of Defense under Office o...
| Main Authors: | , , |
|---|---|
| Format: | Working Paper |
| Language: | en_US |
| Published: |
MIT Artificial Intelligence Laboratory
2008
|
| Online Access: | http://hdl.handle.net/1721.1/41140 |
| _version_ | 1811097759967608832 |
|---|---|
| author | Hewitt, Carl Attardi, Giuseppe Lieberman, Henry |
| author_facet | Hewitt, Carl Attardi, Giuseppe Lieberman, Henry |
| author_sort | Hewitt, Carl |
| collection | MIT |
| description | This report describes research conducted at the Artificial Intelligence Laboratory of the Massachusetts Institute of Technology. Support for the laboratory's artificial intelligence research is provided in part by the Advanced Research Projects Agency of the Department of Defense under Office of Naval Research contract N00014-75-c-0522. |
| first_indexed | 2024-09-23T17:04:29Z |
| format | Working Paper |
| id | mit-1721.1/41140 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T17:04:29Z |
| publishDate | 2008 |
| publisher | MIT Artificial Intelligence Laboratory |
| record_format | dspace |
| spelling | mit-1721.1/411402019-04-10T23:12:19Z Specifying and Proving Properties of Guardians for Distributed Systems Hewitt, Carl Attardi, Giuseppe Lieberman, Henry This report describes research conducted at the Artificial Intelligence Laboratory of the Massachusetts Institute of Technology. Support for the laboratory's artificial intelligence research is provided in part by the Advanced Research Projects Agency of the Department of Defense under Office of Naval Research contract N00014-75-c-0522. In a distributed system where many processors are connected by a network 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 modular fashion. We have developed 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. MIT Artificial Intelligence Laboratory 2008-04-10T16:03:55Z 2008-04-10T16:03:55Z 1979-05 Working Paper http://hdl.handle.net/1721.1/41140 en_US MIT Artificial Intelligence Laboratory Working Papers, WP-172a application/pdf MIT Artificial Intelligence Laboratory |
| 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/41140 |
| work_keys_str_mv | AT hewittcarl specifyingandprovingpropertiesofguardiansfordistributedsystems AT attardigiuseppe specifyingandprovingpropertiesofguardiansfordistributedsystems AT liebermanhenry specifyingandprovingpropertiesofguardiansfordistributedsystems |