Circularity, event structures, and contracts
Sept 11, 12.00
Aula C – Palazzo delle Scienze – Cagliari
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