[PhD position 2022] Non-Aggregative Resource Logic : Models and Calculi
Keywords:
semantics, proof theory, resource logics, non-aggregative composition.
Contact
Didier GALMICHE
(galmiche@loria.fr)
Daniel MERY
(dmery@loria.fr)
Summary
In this PhD, we focus on non-aggregative extensions of separation logics (like SL and BI) and their related resource models.
We shall:
- study proof new resource monoids in which the composition cannot be reduced to the disjoint union of partial functions, starting with extensions and variants of the standard memory heap model of SL;
- propose new resource logics in adequacy with the studied non-aggregative resource models;
- devise non-aggregative extensions of intuitionistic SL in which the preorder on the resources is not derivable from resource composition;
- define non-orthogonal combinations of modals logics (e.g., with temporal modalities) and resource logics.
Scientific Context
Nowadays computer systems are highly complex. Most of them are intrinsically distributed, dynamically and reconfigurable (Big Data, Internet of Things, Cloud Computing) and concurrent at both the physical level (CPU cores) and the logical level (threads). This level of complexity raises important technical problems. For instance, how to ensure that a system consisting of a huge multitude of heterogeneous components, built by different developers, provides the expected services? How to ensure that the components do not block waiting one for another (deadlock), or that one component has to wait indefinitely (denial of service)? How to check that the update of a component’s software does not leak confidential information to third parties?
Understanding complex systems is only possible due to their modularity and the components of a modular system can be viewed, at a higher level of abstraction, as resources, that can be either static or dynamic (a piece of data or a process), physical or logical (CPUs or threads), having simple atomic (a memory cell) or more elaborated structure (such as a linked list or a pipeline). The main operation on a resource domain is composition, formally understood as the product of a partial monoid.
The resource domains having received most attention so far have aggregative composition operations, i.e. composition operations that behave like unions of disjoint sets, as in Separation and Bunched Logics [5,8]. As a typical example of aggregative composition, the heap memory of a program can be modeled by a partial function (from addresses to values) and composition of two heaps is the union of partial functions on disjoint domains. On the other hand, there are many examples of composition operators that are non-aggregative, for instance parallel composition of concurrent processes modeled as finite-state machines or composition of services with common interfaces in a distributed cloud-based application.
Subject and Goals
Some of the algebraic (equational) properties of aggregative compositions, i.e. compositions which obey the principle that the whole is the sum of its parts, have already been considered in existing works [3,7]. However, because the aggregative nature of a composition operator cannot be fully understood in terms of its equational properties alone, we need to introduce more structural aspects like preordering the resources or measuring their size. For instance, an expected property of an aggregative operator is that it should keep its operands as discernable parts of its result.
It should also make the whole composite bigger than any of its parts. However, many natural resource compositions do not follow those principles. For an intuitive example, consider a merging composition about dual resources that annihilate each other (like particles and anti-particles in physics). Merging a resource (particle) a with its dual resource (anti-particle) b, we get the empty resource e (intangible amount of energy). Obviously, the size of the composition a∗b is not bigger than the size of a or the size of b, and only looking at e, one cannot tell if it is the result of a∗b, or of the merging of another dual pair c and d.
A first goal of this PhD is to investigate non-aggregative models of resource composition and try to devise sound and (hopefully) complete corresponding non-aggregative logics.
Existing works that go beyond the standard heap model of Separation Logic (SL) like [6] and [9] mostly explore non-cancellative extensions of classical SL. One reason for the classical bias is that the intuitionistic version of the points-to predicate can easily be characterized in the classical fragment, making intuitionistic SL rather uninteresting. This situation follows from the choice of heap inclusion as the natural preordering relation on heaps. Because heap inclusion is fully derivable from heap extension ( h ⊆ h’ ⇔ ∃h”.h∗h”=h’ ), the aggregative nature of heap composition leads to an intuitionistic separation which is much weaker than its classical counterpart. (e.g. the implication A ∗ B → A ∧ B is valid).
A second goal of this PhD is to study non-aggregative extensions of intuitionistic SL with preorders not fully derivable from resource composition.
Not all interesting aspects of non-aggregative models can be formalized solely in terms of separation connectives. For instance, time and space distributions are in fact better handled via modalities [1,2,4]. Current works mixing modal and resource logics rely on models in which the modalities are interpreted over an accessibility relation that is completely independent of the preordering relation over which the resources are interpreted. Such an orthogonal view of combination helps reusing existing techniques from both fields, but makes it more difficult for the resulting logics to deal with properties involving the interplay of modal and resource aspects. For example, in a temporal extensions of BI, the resources are distributed over points in time at which they are considered to be available. The formula A ∗ (A −∗ B) thus means that if A is satisfied at point t with resources r1 and A −∗ B is satisfied at point t with resources r2, then B should be satisfied at point t with resources r1 ∗ r2. It is easy to see that the interpretation of the resource sensitive connectives does not depend on time. Changing the conclusion to “then B should be satisfied at point t + |r1 |” would allow for a more interacting example where the satisfiability (availability in time) of B would depend on the size of r1 (meaning that the bigger A is, the longer it takes to produce B).
A third goal of this PhD is to consider interacting combinations of modal and (non-aggregative) resource logics.
References
[1] Gabrielle Anderson and David Pym. A calculus and logic of bunched resources and processes. TCS, 614(C):63–96, February 2016.
[2] Stephen Brookes and Peter W. O’Hearn. Concurrent separation logic. ACM SIGLOG News, 3(3):47–65, August 2016.
[3] James Brotherston and Jules Villard. Parametric Completeness for Separation Theories. In POPL, pages 453–464. ACM, 2014.
[4] Jean-René Courtault, Didier Galmiche, and David Pym. A logic of separating modalities. Theor. Comput. Sci., 637(C):30–58, July 2016.
[5] Didier Galmiche, Daniel Méry, and David J. Pym. The semantics of BI and Resource Tableaux. MSCS, 15(6):1033–1088, 2005.
[6] Jonas Braband Jensen and Lars Birkedal. Fictional separation logic. In Helmut Seidl, editor, Programming Languages and Systems, pages 377–396, Berlin, Heidelberg, 2012. Springer Berlin, Heidelberg.
[7] Dominique Larchey-Wendling and Didier Galmiche. Looking at separation algebras with boolean bi-eyes. In Josep Díaz, Ivan Lanese, and Davide Sangiorgi, editors, TCS 2014, volume 8705 of LNCS, pages 326–340. Springer, 2014.
[8] Peter W. O’Hearn, John C. Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In Proceedings of the 15th International Workshop on Computer Science Logic, CSL ’01, pages 1–19, 2001.
[9] Viktor Vafeiadis and Chinmay Narayan. Relaxed separation logic : A program logic for c11 concurrency. In OOPSLA 2013, OOPSLA ’13, page 867–884, New York, NY, USA, 2013. Association for Computing Machinery.
Hosting team
The PhD position is proposed by the TYPES of LORIA research lab.
Skills and profile
- Required qualification: Master in Computer Science (or equivalent)
- Knowledge in the following fields will be appreciated: logic, proof theory, semantics, programming (C, CAML, Java, Python)
Additional information
Duration: 3 years
Starting date: between Oct. 1st 2022 and Dec. 1st 2022
How to apply
Send the following documents to
galmiche@loria.fr
and
dmery@loria.fr
- a CV
- a motivation letter
- your degree certificates and transcripts for Bachelor and Master (or equivalent)
