Abstract Specifications for Concurrent Maps Shale Xiong, Pedro da Rocha Pinto, Gian Ntzik and Philippa Gardner 53 DTRS17-1.pdf Despite recent advances in reasoning about concurrent data structure libraries, the largest implementations in java.util.concurrent have yet to be verified. The key issue lies in the development of modular specifications, which provide clear logical boundaries between clients and implementations. A solution is to use recent advances in fine-grained concurrency reasoning, in particular the introduction of abstract atomicity to concurrent separation logic reasoning. We present two specifications of concurrent maps, both providing the clear boundaries we seek. We show that these specifications are equivalent, in that they can be built from each other. We show how we can verify client programs, such as a concurrent set and a producer-consumer client. We also give a substantial first proof that the main operations of ConcurrentSkipListMap in java.util.concurrent satisfy the map specification. This work demonstrates that we now have the technology to verify the largest implementations in java.util.concurrent.

]]> A Linear Decomposition of Multiparty Sessions for Safe Distributed Programming Alceste Scalas, Raymond Hu, Ornela Dardha and Nobuko Yoshido 73 DTRS17-2.pdf Multiparty Session Types (MPST) is a typing discipline for message-passing distributed processes that can ensure properties such as absence of communication errors and deadlocks, and protocol conformance. Can MPST provide a theoretical foundation for concurrent and distributed programming in "mainstream" languages?

We address this problem by (1) developing the first encoding of a full-fledged multiparty session pi-calculus into standard linear pi-calculus, and (2) using the encoding as the foundation of a practical toolchain for safe multiparty programming in Scala.Our encoding is type-preserving and operationally sound and complete. Importantly for distributed applications, it preserves the choreographic nature of MPST and illuminates that multiparty sessions (and their safety properties) can be precisely represented with a decomposition into binary linear channels. Previous works have only studied the relation between (limited) multiparty sessions and binary sessions by orchestration means.

We exploit these results to implement an automated generation of Scala APIs for multiparty sessions. These APIs act as a layer on top of existing libraries for binary communication channels: this allows distributed multiparty systems to be safely implemented over binary transports, as commonly found in practice. Our implementation is also the first to support distributed multiparty delegation: our encoding yields it for free, via existing mechanisms for binary delegation.

]]> Self-attachment: A self-administrable intervention for chronic anxiety and depression Abbas Edalat 16 DTRS17-3.pdf There has been increasing evidence to suggestthat the root cause of much mental illness lies in a sub-optimal capacity for affect regulation. Cognition and emotion are intricately linked and cognitive deficits, which are characteristic of many psychiatric conditions, are often driven by affect dysregulation, which itself can usually be traced back to sub-optimal childhood development as supported by Attachment Theory. Individuals with insecure attachment types in their childhoods are prone to a variety of mental illness, whereas a secure attachment type in childhood provides a secure base in life. We therefore propose a holistic approach to tackle chronic anxiety and depression, typical of Axis II clinical disorders, which is informed by the development of the infant brain in social interaction with its primary care-givers. We formulate, in a self-administrable way, the protocols governing the interaction of a securely attached child with its primary care-givers that produce the capacity for affect regulation in the child. We posit that these protocols construct, by neuroplasticity and long term potentiation, new optimal neural pathways in the brains of adults with insecure childhood attachment that suffer from mental disorder. This procedure is called self-attachment and aims to help the individuals to create their own attachment objects in the form of their adult self looking after their inner child.

]]> Multiparty Session Types, Beyond Duality Alceste Scalas, Nobuko Yoshida 20 DTRS17-4.pdf Multiparty Session Types (MPST) are a well-established typing discipline for message-passing processes interacting on sessions involving two or more participants. Session typing can ensure desirable properties: absence of communication errors and deadlocks, and protocol conformance. However, existing MPST works provide a subject reduction result that is arguably (and sometimes, surprisingly) restrictive: it only holds for typing contexts with strong duality constraints on the interactions between pairs of participants. Consequently, many "intuitively correct" examples cannot be typed and/or cannot be proved type-safe. We illustrate some of these examples, and discuss the reason for these limitations. Then, we outline a novel MPST typing system that removes these restrictions.

]]> TaLoS: Secure and Transparent TLS Termination inside SGX Enclaves Pierre-Louis Aublin, Florian Kelbert, Dan O'Keeffe, Divya Muthukumaran, Christian Priebe, Joshua Lind, Robert Krahn, Christof Fetzer, David Eyers, Peter Pietzuch 4 DTRS17-5.pdf We introduce TaLoS , a drop-in replacement for existing transport layer security (TLS) libraries that protects itself from a malicious environment by running inside an Intel SGX trusted execution environment. By minimising the amount of enclave transitions and reducing the overhead of the remaining enclave transitions, TaLoS imposes an overhead of no more than 31% in our evaluation with the Apache web server and the Squid proxy.

]]> Differentiation in Logical Form Abbas Edalat and Mehrdad Maleki 16 DTRS17-6.pdf We introduce a logical theory of differentiation for a real-valued function on a finite dimensional real Euclidean space. A real-valued continuous function is represented by a localic approximable mapping between two semi-strong proximity lattices, representing the two stably locally compact Euclidean spaces for the domain and the range of the function. Similarly, the Clarke subgradient, equivalently the L-derivative, of a locally Lipschitz map, which is non-empty, compact and convex valued, is represented by an approximable mapping. Approximable mappings of the latter type form a bounded complete domain isomorphic with the function space of Scott continuous functions of a real variable into the domain of non-empty compact and convex subsets of the finite dimensional Euclidean space partially ordered with reverse inclusion. Corresponding to the notion of a single-tie of a locally Lipschitz function, used to derive the domain-theoretic L-derivative of the function, we introduce the dual notion of a single-knot of approximable mappings which gives rise to Lipschitzian approximable mappings. We then develop the notion of a strong single-tie and that of a strong knot leading to a Stone duality result for locally Lipschitz maps and Lipschitzian approximable mappings. The strong single-knots, in which a Lipschitzian approximable mapping belongs, are employed to define the Lipschitzian derivative of the approximable mapping. The latter is dual to the Clarke subgradient of the corresponding locally Lipschitz map defined domain-theoretically using strong single-ties. A stricter notion of strong single-knots is subsequently developed which captures approximable mappings of continuously differentiable maps providing a gradient Stone duality for these maps. Finally, we derive a calculus for Lipschitzian derivative of approximable mapping for some basic constructors and show that it is dual to the calculus satisfied by the Clarke subgradient.

]]> Decidability of consistency of function and derivative information for a triangle and a convex quadrilateral Abbas Edalat 11 DTRS17-7.pdf Given a triangle in the plane, a planar convex compact set and an upper and and a lower bound, we derive a linear programming algorithm which checks if there exists a real-valued Lipschitz map defined on the triangle and bounded by the lower and upper bounds, whose Clarke subgradient lies within the convex compact set. We show that the problem is in fact equivalent to finding a piecewise linear surface with the above property. We extend the result to a convex quadrilateral in the plane. In addition, we obtain some partial results for this problem in higher dimensions.

]]> Session-ocaml: a Session-based Library with Polarities and Lenses Keigo Imai, Nobuko Yoshida, Shoji Yuen 25 DTRS17-8.pdf We propose session-ocaml, a novel library for session-typed concurrent/distributed programming in OCaml. Our technique solely relies on parametric polymorphism, which can encode core session type structures with strong static guarantees. Our key ideas are: (1) polarised session types, which give an alternative formulation of duality enabling OCaml to automatically infer an appropriate session type in a session with a reasonable notational overhead; and (2) a parameterised monad with a data structure called "slots" manipulated with lenses, which can statically enforce session linearity and delegations. We show applications of session-ocaml including a travel agency usecase and an SMTP protocol.

]]>