Post date: 05-Sep-2012 08:36:33
Upcoming Seminar
Circularity, event structures, and contracts
Sept 11, 12.00
Aula C - Palazzo delle Scienze - Cagliari
Tiziana Cimoli
Dipartimento di Matematica e Informatica - Università degli Studi di Cagliari
Abstract. Contracts will play an increasingly important role in the specification and implementation of distributed (cloud) systems. Quoting from [1], “Absent radical improvements in security technology, we expect that users will use contracts and courts, rather than clever security engineering, to guard against provider malfeasance”. Contracts describe the promised behavior of a software agent, from the point of view of the actions it may perform, the interactions it may participate into, and its goals. A primary use of contracts if that of postponing actual interaction with other agents until an agreement on the mutually promised behaviour has been found. As in the real world, promises are not always kept by software systems, and so contracts may be helpful also after the agreement to disciplinate the interaction among agents, and to establish liability in case of violations.
At a very abstract level, a contract can be seen as sets of events, together with relations to specify the causal dependencies and the conflicts between events. This seems to suggest event structures - one of the fundamental causal models for concurrency - as a natural candidate for representing contracts. For instance, one can interpret the enabling b|-a of a stable event structure as the contract clause “I will do a after you have done b”.
However, event structures do not capture a crucial aspect of contracts, i.e. the capability of reaching an agreement in the presence of circularity in the declared promises. For instance, one would expect that the contract where A promises a in change of b, and B promises b in change of a, has an agreement. This contrasts with the fact that the event structure with enablings b|-a and a|-b has only one configuration - the empty set. This is because a|-b actually models the fact that b may only happen after a has been done, and b|-a as the fact that a may happen after b - and so neither a nor b can happen. Of course, A could simply declare to do a, without asking b to be performed first - but this would not protect A from a misbehaving B.
To reconcile causality with circularity, A could relax her contract, i.e. she could do a in change of the promise of B to do b. In this case A can safely do the first step, because either B does b, or he will be culpable of a contract violation.
In this talk we present an extension of event structures which allows for this kind of reasoning. The contract a||-b (intuitively, “I will do a if you promise to do b”) reaches an agreement with the dual contract b||-a, while protecting the participant who offers it. We characterise configurations of these event structures as provability of formulae in the contract logic PCL, an extension of intuitionistic logic with a “contractual implication” connective.
We then focus on the problem of determining, in any state of the execution of a contract, which events have to be done next. This problem is trivial in classical event structures (one has to do the events whose causes have already been done), while it becomes relevant in the presence of circularity: indeed, before performing an event a (whose causes have not already been done) one has to be sure that its causes will be done, eventually in the future. Also in this case we devise a logical characterisation via an encoding in the logic PCL.
References
[1] Michael Armbrust, Armando Fox, Rean Griffith, Anthony D. Joseph, Randy Katz, Andy Konwinski, Gunho Lee, David Patterson, Ariel Rabkin, Ion Stoica, Matei Zaharia. A View of Cloud Computing. Communications of the ACM, Vol. 53 No. 4, Pages 50-58, 2010