dataesr/scientific-paragraphs-categorization huggingface dataset:
Deductive Verification of C+MPI Code This approach directly verifies C+MPI programs against session types  [Honda et al. , 2012 , Marques et al. , 2013b , López et al. , 2015] , in contrast with Session C where programmers use a particular library of communication primitives. To verify the conformance of C+MPI programs against protocol specifications the programmer starts by capturing the application's communication global protocol description. Afterwards, the protocol is translated into a term written in the language of VCC  [Cohen et al. , 2009] , a software verifier tool for the C programming language (refer to the example below). The translation is done automatically using a tool that verifies that the protocol is well formed, guaranteeing global deadlock freedom. The C+MPI code imports the protocol definition (in VCC form) and a VCC-annotated MPI library with session type con-tracts for the various MPI primitives.
Depending on the specifics of the C code, further manual annotations may be required. In this setting, VCC is invoked to check whether the C code follows the communication type. The overall workflow process is depicted in Figure  4. 1. The verification deals with point-to-point and collective operations. For that, the protocol specification departs from Multiparty Session Types and Scribble by introducing collective decision primitives, allowing for behaviors where all participants decide to enter or to leave a loop, or to choose one of two branches of a choice input. These two patterns are impossible to describe in Scribble, but are a standard practice in C+MPI programs. The communication types language includes specific MPI collective operations, as well as a dependent functional type constructor.
The verification process checks the program from MPI initialization (call to MPI_Init) to shutdown (MPI_Finalize). There is the need to add state and behavior to perform the verification. This is known as ghost data and code, and is only available for the verification process. A ghost type_func function, representing the protocol, parametric on the rank, returns the endpoint projection of the global type for a given rank. This endpoint type is assigned to a ghost variable and the verification proceeds by progressively reducing the protocol, i. e. , by changing the ghost variable through the contracts of MPI primitives or as a result of the annotations that handle program control flow. The goal is that the ghost variable reaches a state congruent to end() at the shutdown point (the call to MPI_Finalize).
As for control flow, collective choices, and loops in particular, direct annotations are necessary in the program body. These are partially generated by a tool. Here, we focus now on its meaning, using the collective loop of our running example. The fragment illustrates the extraction of the protocols corresponding to the loop body and its continuation from the endpoint type stored in ghost variable type. The protocol for the body must be a loop type. The verification procedure asserts that the loop protocol body is reduced to a term congruent to end(). After the loop, verification proceeds by using the loop continuation as the type. The VCC theory put forward by  Marques et al. [2013a]  is divided in two parts: the first is a contract-annotated version of the MPI function signatures that ensures the conformance of the program operations against a protocol; the second encodes the type reduction relation (omitted here for brevity).
Verifying the Customer-Agency C+MPI program using VCC Our running example protocol can be sketched using a VCC datatype value as follows. The function contains the global type ready to be projected, depending on the rank parameter. In what follows we present an excerpt of the annotations required to the C+MPI program presented in the beginning of this section. The ghost annotations inserted into the C+MPI code introduce the ghost variable type, projecting it for a particular rank. The verification proceeds, either directed by the MPI function contract annotations or by the manual annotations inserted before the loops and before the collective choices. More sophisticated constructs, here omitted since they are not used in our running example, include collective operations and foreach loops.
MPI Code Generation A protocol-driven MPI code generation framework [Pabble-MPI] was presented by  Ng et al. [2015]  for type-safe and deadlock-free MPI programs based on Parameterised Multiparty Session Types  [Deniélou et al. , 2012]  using the Pabble protocol description language  [Ng and Yoshida, 2015] , which itself is based on Scribble. The code generation process starts with the definition of the global topology using a protocol specification language based on parameterised multiparty session types (MPST). From this, an MPI parallel program backbone is automatically generated. The backbone code can then be merged with the sequential code describing the application behaviour, resulting in a complete MPI program. This merging process is fully automated through the use of an aspect-oriented compilation approach.
Related Work Session C needs to be extended to support more conventional parallel programming runtime library. Message Passing Interface (MPI) has been identified as the ideal API to target because of its comprehen-siveness, because it is standardized, and, to a lesser extent, because of its popularity in the HPC community. Also, the approach of Session C is only as useful as the expressiveness of the protocol language (Scribble) being type-checked against. In order to support MPI as the programming API for Session C, Scribble is currently being extended to a dependent language, with the primary aim of supporting a scalable way of addressing participants using numeric indexes. The challenges of this is to keep type checking decidable, while increasing the complexity of the parallel programming/MPI primitives that Session C supports.
Global Types for MAS Monitoring Global types can be easily represented as cyclic Prolog terms, and a mechanism for verifying that a sequence of messages complies with a global type has been designed and implemented in Prolog. By exploiting these features, a monitor has been developed on top of Jason; such a monitor is able to verify at run-time that the actual conversation among agents in the MAS complies to the interaction protocol specified by a global type in the formalism described in this section. Interactions. An interaction occurring between two agents is represented as a 4-tuple consisting of two agent identifiers (the sender and the receiver of the message), the performative (explained below) expressed in some agent communication language the agents agree upon, such as FIPA-ACL [Foundation for Intelligent Physical Agents] or KQML  [Mayfield et al.
However their solution is less simple than the specification presented in the previous section. Furthermore, the notion of global type as described here is more amenable to be directly translated in Prolog as a finite collection of unification equations having regular terms as solutions. An interesting proposal for overcoming the limitations of dynamic protocol verification based on a centralized monitor is proposed by Chen et al. [2012]. There, a formal model of run-time safety enforcement for large-scale, cross-language distributed applications with possibly untrusted endpoints is proposed, whose underlying theory is based on multiparty session types with logical assertions (MPSA). MPSA is an expressive protocol specification language that supports run-time validation through monitoring.
Singularity OS  [Hunt et al. , 2005 , Fähndrich et al. , 2006, Singularity OS]  is the prototype of a reliable operating system where softwareisolated processes (SIPs) share the same address space, called exchange heap. Process interaction occurs solely through message exchange over asynchronous, FIFO channels and the communication overhead is reduced thanks to copyless message passing: only pointers to messages are physically exchanged between processes. Static analysis enforces process isolation, that is, every process can only access the memory it owns in an exclusive manner. Programs running in Singularity OS are written in Sing # , a programming language derived from C # specifically designed for developing Singularity applications. In this chapter we review the support for behavioural typing provided by Sing # ( §6.
Channel Contracts in Sing # In Singularity OS, channels are formed as pairs of related endpoints, called the channel peers. A message sent over a peer is received from the other peer. Each peer is equipped with a FIFO buffer storing the messages sent to that peer that have not been read yet. This means that communication is asynchronous (send operations are non-blocking) and process synchronization is realized via handshaking protocols. Channel communication is, indeed, ruled by channel contracts, verified at compile-time, that describe messages, message argument types, and valid message interaction sequences as finite state machines. In essence, channel contracts are a syntactic variation of session types. We now take a closer look at Sing # by means of the Customer-Agency example. The pseudocode snippet in Figure  6.
The in ExHeap annotation states that a name denotes a pointer to an object allocated on the exchange heap. Regarding communications, the correctness of this code fragment relies on the assumption that the process(es) using the peer endpoints of c and d are able to deal with the message types as they are received/sent from within Agency. To this end, Sing # provides channel contracts describing the communication patterns that are permitted on a given endpoint. Consider, for example, the contracts for the Costumer-Agency example: A contract is made of a finite set of message specifications and a finite set of states linked by transitions. Each message specification starts with the keyword message, followed by the tag of the message and the type of its arguments. The state of an endpoint is determined by the state of the contract associated to it.
From the previous discussion, it is sensible to formalize Sing # exploiting a process calculus equipped with an apt session type system for session types. There are, indeed, analogies between contracts and endpoint types: the contract defines an interaction between two processes in terms of states and transitions, from the viewpoint of one of the two processes; the session type defines the actions of a single process taking part to the interaction; the exporting and importing views of a contract correspond to the notion of duality in session types. Bono et al. [2011]  have formalized a session-oriented process calculus in which it is straightforward to encode the Costumer-Agency example.
Having pinpointed the actual reason why the function leak is faulty is the main contribution of the formalization of Sing #  [Bono et al. , 2011]. Fähndrich et al. [2006]  address how the language, verification, and runtime system features of copyless message passing make it suited for actual use as the only mechanism of communication between processes in Singularity. The authors show, by means of an advanced programming language and appropriate verification techniques, that it is possible to yield strong system-wide invariants that endow efficient communication and low-overhead, software-based process isolation. An (informal) overview of Singularity OS specifications is given by  Hunt et al. [2005]. Bono et al. [2011]  present a calculus that models a form of process interaction based on copyless message passing, in the style of Singularity OS.
Procedure checkPrice implements protocol CheckPrice. The procedure is declared together with the processes and sessions it uses, respectively c,a and s (lines 22-23). All parameters are behaviorally typed, indicating which protocol each session should implement and which role each process plays in the sessions. In this case, the declaration states that session s implements protocol CheckPrice using process c as the customer and process a as the agency. The body of checkPrice follows the structure of the protocol CheckPrice (lines 25-42). Note the usage of concrete data values and the conditional construct if since this is actual code, not merely a protocol description. Using Chor, the choreography above can be automatically translated into an executable implementation in the Jolie language [development team] equivalent to that presented in §7.
Scribble The Scribble project  [Honda et al. , 2014 [Honda et al. , , 2011 ] is a collaboration between session types researchers and architects and engineers from industry towards the application of session types principles and techniques to current engineering practices. Building on the theory of multiparty session types (MPST)  [Honda et al. , 2008 , Bettini et al. , 2008b] , this ongoing work tackles the challenges of adapting and implementing session types to meet real-world usage requirements. This section gives an overview of the current version of the Scribble framework for the MPST-based development of distributed software. In the context of Scribble, we use the terms session and conversation interchangeably. The main elements of the Scribble framework are as follows. The Scribble language is a platform-independent description language for the specification of asynchronous, multiparty message passing protocols  [Honda et al.
, 2014 [Honda et al. , , 2011]]. Scribble may be used to specify protocols from both the global (neutral) perspective and the local perspective of a particular participant (abstracted as a role); at heart, the Scribble language is an engineering incarnation of the notation for global and local types in formal MPST systems and their correctness conditions. The Scribble Conversation API provides the local communication operations for implementing the endpoint programs for each role natively in various mainstream languages. The current version of Scribble supports Java and Python Conversation APIs with both standard socket-like and event-driven interfaces for initiating and conducting conversations. The Scribble Runtime is a local platform library for executing Scribble endpoint programs written using the Conversation API.
The Runtime includes a conversation monitoring service for dynamically verifying  [Hu et al. , 2013 , Bocchi et al. , 2013 , Neykova et al. , 2013 , Demangeon et al. , 2015]  the interactions performed by the endpoint against the local protocol for its role in the conversation. In addition to internal monitors at the endpoints, Scribble from Agency, the exchange of address details and the ticket dispatch date is now conducted between Customer and Service, representing the transport service being brokered by Agency. The Scribble is read as follows: • The first line declares the Scribble module name. Although this example is self-contained within a single module, Scribble code may be organized into a conventional hierarchy of packages and modules. Importing payload type and protocol declarations between modules is useful for factoring out libraries of common payload types and subprotocols.
• The design of the Scribble language focuses on the specification of protocol structures. With regards to the payload data that may be carried in the exchanged messages, Scribble is designed to work orthogonally with external message format specifications and data types from other languages. The type declaration on Line 3 declares a payload type based on Java object serialization format, specifically java. lang. Double objects, whose definition (i. e. class) is to be imported from the file rt. jar, and is aliased as Double within this Scribble module. Data type formats from other languages, as well as XML or various IDL based message formats, may be used similarly. A single protocol definition may feature a mixture of message types defined by different formats. • Line 8 declares the signature of a global protocol called BookJourney.
This protocol involves three roles: Customer (C), Agency (A), and Service (S). • Lines 9-24 define the interaction structure of the protocol. Line 11 specifies a basic message passing action. query(journey:String) is a message signature for a message with header (label) journey, carrying one payload element within the parentheses. A payload element is an (optional) annotation followed by a colon and the payload type, e. g. journey details are recorded in a String. This message is to be dispatched by C to be received by A. • The outermost construct of the protocol body is the rec block with label Loop. Similarly to labeled blocks in e. g. Java, the occurrence of a continue for the same label within the block causes the flow of the protocol to return to the start of the block. The first choice within the rec, decided by • To developers, Scribble is a new language to be learned and understood, particularly since most developers are not accustomed to formal protocol specification in this manner.
In comparison to languages implemented from binary session types, such as SJ and Mungo ( §2. 2) or Sing # (Chapter 6), this additional step is required to derive local specifications for the endpoint implementation of each role process from the central global protocol specification. Scribble projection follows the standard MPST algorithmic projections, with extensions for the additional features of Scribble, such as the subprotocols and conversation interrupts mentioned above. Figure  8. 3 lists the local protocol generated by the Scribble tools as the projection of the BookJourney for the Customer role, identified in the local protocol signature as the self role. Projection preserves the dependencies of the global protocol, such as the payload types used, and the core interaction structures in which the target role is involved, e.
g. the rec and choice blocks, as well as payload annotations and similar protocol details. The well-formedness conditions on global protocols allow the projection to safely discard all message actions not involving C (i. e. messages between A and S). As for the binary session languages cited above, it is possible to statically type check role implementations written in endpoint languages with appropriate MPST programming primitives against the local protocols following the standard MPST theory: if the endpoint program for every role is correct, then the correctness of the whole multiparty system is guaranteed. The endpoint languages used in the Scribble industry projects, however, are mainstream engineering languages like Java and Python that lack the features, such as first-class communication channels with linear resource typing or object alias restriction, required to make static session typing feasible.
In Scribble practice, the Conversation API is used to perform the relevant conversation operations natively in these languages, making static MPST type checking intractable. In general, distributed systems are often implemented in a mixture of languages, including dynamically typed languages (e. g. Python), and techniques such as event-driven programming, for which the static verification of strong safety properties is acknowledged to be difficult. For these reasons, the Scribble framework, differently from the above session languages, is designed to focus on dynamic verification of endpoint behavior  [Hu et al. , 2013]. Endpoint monitoring by the local Conversation Runtime is performed by converting local protocols to communicating finite state automata, for which the accepted languages correspond to the I/O action traces permitted by the protocol.
The loop is thus specified by the mutual recursion between these two protocol declarations. The final example demonstrates the Scribble feature for asynchronously interruptible conversations. Unlike the previous features, which involve the integration of session types with useful, general programming language features (code abstraction and parameterization), conversation interrupts require extensions to the core design of session types  [Hu et al. , 2013]. The motivation for interrupts comes from our collaboration use cases, featuring patterns such as asynchronously interruptible streams and interaction timeouts,which could not be directly expressed in the standard MPST formulations. Figure  8. 6 gives a very simple revision of the ServiceCall protocol that allows the Client to cancel the call by interrupting the Server's reply.
Related Work The development of the Scribble framework and its application in realworld use cases is ongoing work. The two main use case projects men-tioned in the above are: Savara is a JBoss project developed by Red Hat. Savara relies on Scribble as an intermediate language for representing protocols, to which high-level notations, such as BPMN2, are translated to perform endpoint projections and various refactoring tasks. Savara provides a suite of tools for testing of service specifications against the initial project requirements. The testing is based on simulations between the former, represented in Scribble, and the latter, expressed as sequence diagram traces. The Ocean Observatories Initiative is an NSF-funded project to develop the infrastructure for the remote, real-time acquisition and delivery of data from a large sensor network deployed in ocean environments to users at research institutions.
The Scribble framework, including Conversation Runtime monitoring, has been integrated into the Python-based OOI platform. So far, the OOI cyberinfrastructure is mainly running on an RPC-based architecture. The current Scribble integration is accordingly primarily used for the specification of RPC service and application protocols, and the dynamic verification of the Python client/server endpoints. Below, we summarize some of the active threads in regards to these projects. • The Savara project is examining formal encodings between the specification languages commonly used in practice and Scribble (the current translation by Savara is not yet formalized), which is motivating further extensions to Scribble, such as dynamic introduction of roles during a conversation and fork-join conversation patterns.
Annotations may be associated to individual messages, interaction steps, control flow structures, roles or protocols as a whole; examples range from basic constraints on specific message values and control flow (e. g. recursion bounds) to more complicated logics for security or contractural obligations of roles. The Scribble framework will accept plugins for parsing and projecting the annotation language, and evaluating the annotations at run-time. This allows the Scribble tools and monitors to be extended modularly with application-and domain-specific annotations, and the dynamic verification approach enables the enforcement of properties that would be difficult or impossible to verify statically without conservative restrictions. • The Savara and OOI use cases implement the Scribble language, meaning the syntax, well-formedness (valid protocol) conditions and projections, as defined by the central language reference.
Both implementations also necessarily conform to baseline communication model of Scribble, namely asynchronous but reliable and role-to-role ordered messaging. The Scribble project is currently working on defining an accompanying Conversation Runtime specification. This will provide the reference for Scribble runtime libraries and platforms, including the specification of the key system protocols for conversation initiation, message formats (conversation and monitoring message meta data) and more advanced features such as conversation delegations  [Hu et al. , 2008]. This work is towards full interoperability of Scribble endpoints running on different platforms, such as the Java and Python platforms of the above use cases, supported by platform-independent monitoring. This interoperability will also extend to safely combining dynamically and statically verified endpoints within conversations.