369 results found
Barwell A, Hou P, Yoshida N, et al., 2023, Designing asynchronous multiparty protocols with crash-stop failures, European Conference on Object-Oriented Programming (ECOOP 2023), Publisher: Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, Pages: 1:1-1:30, ISSN: 1868-8969
Session types provide a typing discipline for message-passing systems. However, most session type approaches assume an ideal world: one in which everything is reliable and without failures. Yet this is in stark contrast with distributed systems in the real world. To address this limitation, we introduce Teatrino, a code generation toolchain that utilises asynchronous multiparty session types(MPST) with crash-stop semantics to support failure handling protocols. We augment asynchronous MPST and processes with crash handling branches. Our approach requires no user-level syntax extensions for global types and features a formalisation of global semantics, which captures complex behaviours induced by crashed/crash handling processes. The sound and complete correspondence between global and local type semantics guarantees deadlock-freedom, protocol conformance, and liveness of typed processes in the presence of crashes. Our theory is implemented in the toolchain Teatrino, which provides correctness by construction. Teatrino extends the Scribble multiparty protocol language to generate protocol-conformingScala code, using the Effpi concurrent programming library. We extend both Scribble and Effpi to support crash-stop behaviour. We demonstrate the feasibility of our methodology and evaluate Teatrino with examples extended from both session type and distributed systems literature.
Castro-Perez D, Yoshida N, 2023, Dynamically Updatable Multiparty Session Protocols Generating Concurrent Go Code from Unbounded Protocols, ISSN: 1868-8969
Multiparty Session Types (MPST) are a typing disciplines that guarantee the absence of deadlocks and communication errors in concurrent and distributed systems. However, existing MPST frameworks do not support protocols with dynamic unbounded participants, and cannot express many common programming patterns that require the introduction of new participants into a protocol. This poses a barrier for the adoption of MPST in languages that favour the creation of new participants (processes, lightweight threads, etc) that communicate via message passing, such as Go or Erlang. This paper proposes Dynamically Updatable Multiparty Session Protocols, a new MPST theory (DMst) that supports protocols with an unbounded number of fresh participants, whose communication topologies are dynamically updatable. We prove that DMst guarantees deadlock-freedom and liveness. We implement a toolchain, GoScr (Go-Scribble), which generates Go implementations from DMst, ensuring by construction, that the different participants will only perform I/O actions that comply with a given protocol specification. We evaluate our toolchain by (1) implementing representative parallel and concurrent algorithms from existing benchmarks, textbooks and literature; (2) showing that GoScr does not introduce significant overheads compared to a naive implementation, for computationally expensive benchmarks; and (3) building three realistic protocols (dynamic task delegation, recursive Domain Name System, and a parallel Min-Max strategy) in GoScr that could not be represented with previous theories of session types.
Ghilezan S, Pantović J, Prokić I, et al., 2023, Precise Subtyping for Asynchronous Multiparty Sessions, ACM Transactions on Computational Logic, Vol: 24, Pages: 1-73, ISSN: 1529-3785
<jats:p> Session subtyping is a cornerstone of refinement of communicating processes: A process implementing a session type (i.e., a communication protocol) <jats:italic>T</jats:italic> can be safely used whenever a process implementing one of its supertypes <jats:italic>T</jats:italic> ′ is expected, in any context, without introducing deadlocks nor other communication errors. As a consequence, whenever <jats:italic>T</jats:italic> ≤ <jats:italic>T</jats:italic> ′ holds, it is safe to replace an implementation of <jats:italic>T</jats:italic> ′ with an implementation of the subtype <jats:italic>T</jats:italic> , which may allow for more optimised communication patterns. We present the first formalisation of the <jats:italic>precise</jats:italic> subtyping relation for <jats:italic>asynchronous multiparty</jats:italic> sessions. We show that our subtyping relation is <jats:italic>sound</jats:italic> (i.e., guarantees safe process replacement, as outlined above) and also <jats:italic>complete</jats:italic> : Any extension of the relation is unsound. To achieve our results, we develop a novel <jats:italic>session decomposition</jats:italic> technique, from <jats:italic>full</jats:italic> session types (including internal/external choices) into <jats:italic>single input/output session trees</jats:italic> (without choices). We cover <jats:italic>multiparty</jats:italic> sessions with <jats:italic>asynchronous</jats:italic> inte
Gheri L, Yoshida N, 2023, Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection, Proceedings of the ACM on Programming Languages, Vol: 7
Multiparty session types (MPST) are a specification and verification framework for distributed message-passing systems. The communication protocol of the system is specified as a global type, from which a collection of local types (local process implementations) is obtained by endpoint projection. A global type is a single disciplining entity for the whole system, specified by one designer that has full knowledge of the communication protocol. On the other hand, distributed systems are often described in terms of their components: a different designer is in charge of providing a subprotocol for each component. The problem of modular specification of global protocols has been addressed in the literature, but the state of the art focuses only on dual input/output compatibility. Our work overcomes this limitation. We propose the first MPST theory of multiparty compositionality for distributed protocol specification that is semantics-preserving, allows the composition of two or more components, and retains full MPST expressiveness. We introduce hybrid types for describing subprotocols interacting with each other, define a novel compatibility relation, explicitly describe an algorithm for composing multiple subprotocols into a well-formed global type, and prove that compositionality preserves projection, thus retaining semantic guarantees, such as liveness and deadlock freedom. Finally, we test our work against real-world case studies and we smoothly extend our novel compatibility to MPST with delegation and explicit connections.
Mezzina CA, Tiezzi F, Yoshida N, 2023, Rollback Recovery in Session-Based Programming, Pages: 195-213, ISBN: 9783031353604
To react to unforeseen circumstances or amend abnormal situations in communication-centric systems, programmers are in charge of “undoing” the interactions which led to an undesired state. To assist this task, session-based languages can be endowed with reversibility mechanisms. In this paper we propose a language enriched with programming facilities to commit session interactions, to roll back the computation to a previous commit point, and to abort the session. Rollbacks in our language always bring the system to previous visited states and a rollback cannot bring the system back to a point prior to the last commit. Programmers are relieved from the burden of ensuring that a rollback never restores a checkpoint imposed by a session participant different from the rollback requester. Such undesired situations are prevented at design-time (statically) by relying on a decidable compliance check at the type level, implemented in MAUDE. We show that the language satisfies error-freedom and progress of a session.
Demangeon R, Yoshida N, 2023, Causal computational complexity of distributed processes, Information and Computation, Vol: 290, ISSN: 0890-5401
This article studies the complexity of π-calculus processes with respect to the quantity of transitions caused by an incoming message. First, we propose a typing system for integrating Bellantoni and Cook's characterisation of polytime computable functions into Deng and Sangiorgi's typing system for termination. We then define computational complexity of distributed messages based on Degano and Priami's causal semantics, which identifies the dependency between interleaved transitions. Next, we apply a necessary syntactic flow analysis to typable processes to ensure a computational bound on the number of distributed messages. We prove that our analysis is decidable; sound in the sense that it guarantees that the total number of messages causally dependent of an input request received from the outside is bounded by a polynomial of the content of this request; and complete, meaning that each polynomial recursive function can be computed by a typable process.
Vasconcelos VT, Martins F, Lopez H-A, et al., 2022, A Type Discipline for Message Passing Parallel Programs, ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, Vol: 44, ISSN: 0164-0925
Ellis S, Zhu S, Yoshida N, et al., 2022, Generic go to go: dictionary-passing, monomorphisation, and hybrid, Proceedings of the ACM on Programming Languages, Vol: 6
Go is a popular statically-typed industrial programming language. To aid the type safe reuse of code, the recent Go release (Go 1.18) published early 2022 includes bounded parametric polymorphism via generic types. Go 1.18 implements generic types using a combination of monomorphisation and call-graph based dictionary-passing called hybrid. This hybrid approach can be viewed as an optimised form of monomorphisation that statically generates specialised methods and types based on possible instantiations. A monolithic dictionary supplements information lost during monomorphisation, and is structured according to the program's call graph. Unfortunately, the hybrid approach still suffers from code bloat, poor compilation speed, and limited code coverage. In this paper we propose and formalise a new non-specialising call-site based dictionary-passing translation. Our call-site based translation creates individual dictionaries for each type parameter, with dictionary construction occurring in place of instantiation, overcoming the limitations of hybrid. We prove it correct using a novel and general bisimulation up to technique. To better understand how different generics translation approaches work in practice, we benchmark five translators, Go 1.18, two existing monomorphisation translators, our dictionary-passing translator, and an erasure translator. Our findings reveal several suggestions for improvements for Go 1.18 - specifically how to overcome the expressiveness limitations of generic Go and improve compile time and compiled code size performance of Go 1.18.
Peters K, Yoshida N, 2022, On the expressiveness of mixed choice sessions, EXPRESS/SOS 2022 : Combined 29th International Workshop on Expressiveness in Concurrency and 19th Workshop on Structural Operational Semantics, Publisher: Open Publishing Association, Pages: 113-130, ISSN: 2075-2180
Session types provide a flexible programming style for structuring interaction, and are used to guarantee a safe and consistent composition of distributed processes. Traditional session types include only one-directional input (external) and output (internal) guarded choices. This prevents the session-processes to explore the full expressive power of the pi-calculus where the mixed choices are proved more expressive than the (non-mixed) guarded choices. To account this issue, recently Casal, Mordido, and Vasconcelos proposed the binary session types with mixed choices (CMV+). This paper carries a surprising, unfortunate result on CMV+: in spite of an inclusion of unrestricted channels with mixed choice, CMV+'s mixed choice is rather separate and not mixed. We prove this negative result using two methodologies (using either the leader election problem or a synchronisation pattern as distinguishing feature), showing that there exists no good encoding from the pi-calculus into CMV+, preserving distribution. We then close their open problem on the encoding from CMV+ into CMV (without mixed choice), proving its soundness and thereby that the encoding is good up to coupled similarity.
Barwell A, Scalas A, Yoshida N, et al., 2022, Generalised multiparty session types with crash-stop failures, International Conference on Concurrency Theory (CONCUR), Publisher: Schloss Dagstuhl, Pages: 35:1-35:25, ISSN: 1868-8969
Session types enable the specification and verification of communicating systems. However, their theory often assumes that processes never fail. To address this limitation, we present a generalised multiparty session type (MPST) theory with crash-stop failures, where processes can crash arbitrarily.Our new theory validates more protocols and processes w.r.t. previous work. We apply minimal syntactic changes to standard session π-calculus and types: we model crashes and their handling semantically, with a generalised MPST typing system parametric on a behavioural safety property. We cover the spectrum between fully reliable and fully unreliable sessions, via optional reliability assumptions, and prove type safety and protocol conformance in the presence of crash-stop failures. Introducing crash-stop failures has non-trivial consequences: writing correct processes that handle all crash scenarios can be difficult. Yet, our generalised MPST theory allows us to tame this complexity, via model checkers, to validate whether a multiparty session satisfies desired behavioural properties, e.g. deadlock-freedom or liveness, even in presence of crashes. We implement our approach using the mCRL2 model checker, and evaluate it with examples extended from the literature
Peters K, Yoshida N, 2022, On the Expressiveness of Mixed Choice Sessions, Electronic Proceedings in Theoretical Computer Science, Vol: 368, Pages: 113-130
Gheri L, Lanese I, Sayers N, et al., 2022, Design-by-contract for flexible multiparty session protocols, European Conference on Object-Oriented Programming (ECOOP 2022), Publisher: Schloss Dagstuhl, Leibniz-Zentrum, Pages: 1-28, ISSN: 1868-8969
Choreographic models support a correctness-by-construction principle in distributed programming. Also, they enable the automatic generation of correct message-based communication patterns from a global specification of the desired system behaviour. In this paper we extend the theory ofchoreography automata, a choreographic model based on finite-state automata, with two key features. First, we allow participants to act only in some of the scenarios described by the choreography automaton. While this seems natural, many choreographic approaches in the literature, andchoreography automata in particular, forbid this behaviour. Second, we equip communications with assertions constraining the values that can be communicated, enabling a design-by-contract approach. We provide a toolchain allowing to exploit the theory above to generate APIs for TypeScript web programming. Programs communicating via the generated APIs follow, by construction, the prescribed communication pattern and are free from communication errors such as deadlocks
Lagaillardie N, Neykova R, Yoshida N, 2022, Stay safe under panic: affine rust programming with multiparty session types, European Conference on Object-Oriented Programming (ECOOP)'22), Publisher: Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik, Pages: 4:1-4:29, ISSN: 1868-8969
Communicating systems comprise diverse software components across networks. To ensure theirrobustness, modern programming languages such as Rust provide both strongly typed channels,whose usage is guaranteed to be affine (at most once), and cancellation operations over binarychannels. For coordinating components to correctly communicate and synchronize with eachother, we use the structuring mechanism from multiparty session types, extending it with affinecommunication channels and implicit/explicit cancellation mechanisms. This new typing discipline,affine multiparty session types (AMPST), ensures cancellation termination of multiple, independentlyrunning components and guarantees that communication will not get stuck due to error or abrupttermination. Guided by AMPST, we implemented an automated generation tool (MultiCrusty) ofRust APIs associated with cancellation termination algorithms, by which the Rust compiler autodetects unsafe programs. Our evaluation shows that MultiCrusty provides an efficient mechanismfor communication, synchronization and propagation of the notifications of cancellation for arbitraryprocesses. We have implemented several usecases, including popular application protocols (OAuth,SMTP), and protocols with exception handling patterns (circuit breaker, distributed logging).
Gheri L, Lanese I, Sayers N, et al., 2022, Design-by-contract for flexible multiparty session protocols (Artifact), ECOOP 2022 (Artifacts Evaluation), Publisher: Schloss Dagstuhl, Leibniz-Zentrum, Pages: 1-5, ISSN: 2509-8195
We introduce CAScr, the first implementationof Scribble (http://www.scribble.org, https://nuscr.dev/) that relies on choreography automata,for deadlock-free distributed programming. CAScrsupports the main theoretical results and construc-tions in the related article. CAScr takes the populartop-down approach to system development, basedon choreographic models, following the originalmethodology of Scribble and multiparty sessiontypes. The top-down approach enables correctness-by-construction: a developer provides a global de-scription for the whole communication protocol;by projecting the global protocol, APIs are gen-erated from local CFSMs, which ensure the safeimplementation of each participant. The theoryof choreography automata in the related articleguarantees deadlock freedom for the distributedimplementation of flexible global protocols. Wetarget web development, supporting in particularthe TypeScript programming language.
Gheri L, Lanese I, Sayers N, et al., 2022, Design-By-Contract for Flexible Multiparty Session Protocols, ECOOP 2022, ISSN: 1868-8969
Choreographic models support a correctness-by-construction principle in distributed programming. Also, they enable the automatic generation of correct message-based communication patterns from a global specification of the desired system behaviour. In this paper we extend the theory of choreography automata, a choreographic model based on finite-state automata, with two key features. First, we allow participants to act only in some of the scenarios described by the choreography automaton. While this seems natural, many choreographic approaches in the literature, and choreography automata in particular, forbid this behaviour. Second, we equip communications with assertions constraining the values that can be communicated, enabling a design-by-contract approach. We provide a toolchain allowing to exploit the theory above to generate APIs for TypeScript web programming. Programs communicating via the generated APIs follow, by construction, the prescribed communication pattern and are free from communication errors such as deadlocks.
Gheri L, Lanese I, Sayers N, et al., 2022, Design-by-Contract for Flexible Multiparty Session Protocols - Choreography Automata for distributed TypeScript programming (Artifact), ECOOP 2022
Barwell AD, Ferreira F, Yoshida N, 2022, Book review, Journal of Logical and Algebraic Methods in Programming, Vol: 125, Pages: 100744-100744, ISSN: 2352-2208
Cutner Z, Yoshida N, Vassor M, 2022, Deadlock-Free Asynchronous Message Reordering in Rust with Multiparty Session Types, 27th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP), Publisher: ASSOC COMPUTING MACHINERY, Pages: 246-261
Graversen E, Phillips I, Yoshida N, 2022, Event structures for the reversible early internal π-calculus, Journal of Logical and Algebraic Methods in Programming, Vol: 124, Pages: 1-46, ISSN: 2352-2208
The 휋-calculus is a widely used process calculus, which models communications between processes and allows the passing of communication links. Various operationalsemantics of the 휋-calculus have been proposed, which can be classified according towhether transitions are unlabelled (so-called reductions) or labelled. With labelled transitions, we can distinguish early and late semantics. The early version allows a processto receive names it already knows from the environment, while the late semantics andreduction semantics do not. All existing reversible versions of the 휋-calculus use reduction or late semantics, despite the early semantics of the (forward-only) 휋-calculusbeing more widely used than the late. We introduce two reversible forms of the internal 휋-calculus; these are the first to use early semantics. The internal 휋-calculus is asubset of the 휋-calculus where every link sent by an output is private, yielding greatersymmetry between inputs and outputs. One of the new reversible calculi uses staticreversibility, where performing an action does not change the structure of the process,and the other uses dynamic reversibility, where performing an action moves it to a separate history. We show an operational correspondence between the two calculi. Forthe static calculus we define denotational event structure semantics, which generate anevent structure inductively on the structure on the process. For the dynamic calculus wedefine operational event structure semantics, which generate an event structure basedon a labelled asynchronous transition system. We describe a correspondence betweenthe resulting event structures.
Aceto L, Bertrand N, Yoshida N, 2021, INTERVIEWS WITH THE 2021 CONCUR TEST-OF-TIME AWARD RECIPIENTS, BULLETIN OF THE EUROPEAN ASSOCIATION FOR THEORETICAL COMPUTER SCIENCE, ISSN: 0252-9742
Yoshida N, Ferreira Ruiz F, Zhou F, 2021, Communicating Finite State Machines and an Extensible Toolchain for Multiparty Session Types, FCT 2021 - 23rd International Symposium on Fundamentals of Computation Theory, Publisher: Springer Verlag, ISSN: 0302-9743
This short article announces the recipients of the CONCUR Test-of-Time Award 2021.
Medic D, Mezzina CA, Phillips I, et al., 2021, Towards a formal account for software transactional memory, Twelfth International Conference on Reversible Computation, Publisher: Springer Verlag, Pages: 255-263, ISSN: 0302-9743
Software transactional memory (STM) is a concurrency con-trol mechanism for shared memory systems. It is opposite to the lockbased mechanism, as it allows multiple processes to access the same setof variables in a concurrent way. Then according to the used policy, theeffect of accessing to shared variables can be committed (hence, madepermanent) or undone. In this paper, we define a formal framework fordescribing STMs and show how with a minor variation of the rules it ispossible to model two common policies for STM: reader preference andwriter preference.
Toninho B, Yoshida N, 2021, On polymorphic sessions and functions: A tale of two (fully abstract) encodings, ACM Transactions on Programming Languages and Systems, Vol: 43, Pages: 1-55, ISSN: 0164-0925
This work exploits the logical foundation of session types to determine what kind of type discipline for the𝜋-calculus can exactly capture, and is captured by, 𝜆-calculus behaviours. Leveraging the proof theoreticcontent of the soundness and completeness of sequent calculus and natural deduction presentations of linearlogic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processesencodings between a polymorphic session 𝜋-calculus and a linear formulation of System F. We are then ableto derive results of the session calculus from the theory of the 𝜆-calculus: (1) we obtain a characterisation ofinductive and coinductive session types via their algebraic representations in System F; and (2) we extend ourresults to account for value and process passing, entailing strong normalisation.
Castro-Perez D, Ferreira Ruiz F, Gheri L, et al., 2021, Zooid: a DSL for certified multiparty computation: from mechanised metatheory to certified multiparty processes, PLDI 2021, Publisher: Association for Computing Machinery (ACM), Pages: 237-251
We design and implement Zooid, a domain specific language for certified multiparty communication, embedded in Coq and implemented atop our mechanisation frame work of asynchronous multiparty session types (the first of its kind). Zooid provides a fully mechanised metatheory for the semantics of global and local types, and a fully verified end-point process language that faithfully reflects the type-level behaviours and thus inherits the global types properties such as deadlock freedom, protocol compliance, and liveness guarantees.
Yoshida N, Cutner Z, 2021, Safe session-based asynchronous coordination in rust, Coordination 2021, Publisher: Springer Verlag, Pages: 80-89, ISSN: 0302-9743
Rust is a popular systems language focused on performance and reliability, with an emphasis on providing “fearless concurrency”. Message passing has become a widely-used pattern by Rust developers although the potential for communication errors leaves developing safe and concurrent applications an unsolved challenge. In this ongoing work, we use multiparty session types to provide safety guarantees such as deadlock-freedom by coordinating message-passing processes. In contrast to previous contributions [22,21,20], our implementation targets asynchronous applications using a sync/await code in Rust. Specifically, we incorporate a synchronous subtyping theory, which allows program optimisation through reordering input and output actions. We evaluate our ideas by developing several representative use cases from the literature and by taking microbenchmarks. We discuss our plans to support full API generation integrating asynchronous optimisations.
Graversen E, Phillips I, Yoshida N, 2021, Event structure semantics of (controlled) reversible CCS, Journal of Logical and Algebraic Methods in Programming, Vol: 121, ISSN: 2352-2208
CCSK is a reversible form of CCS which is causal, meaning that actions can be reversed if and only if each action caused by them has already been reversed; there is no control on whether or when a computation reverses. We propose an event structure semantics for CCSK. For this purpose we define a category of reversible bundle event structures, and use the causal subcategory to model CCSK. We then modify CCSK to control the reversibility with a rollback primitive, which reverses a specific action and all actions caused by it. To define the event structure semantics of rollback, we change our reversible bundle event structures by making the conflict relation asymmetric rather than symmetric, and we exploit their capacity for non-causal reversibility.
Bravetti M, Carbone M, Lange J, et al., 2021, A sound algorithm for asynchronous session subtyping and its implementation, Logical Methods in Computer Science, Vol: 17, Pages: 1-35, ISSN: 1860-5974
Session types, types for structuring communication between endpoints in distributed systems, are recently being integrated into mainstream programming languages. In practice, a very important notion for dealing with such types is that of subtyping, since it allows for typing larger classes of system, where a program has not precisely the expected behaviour but a similar one. Unfortunately, recent work has shown that subtyping for session types in an asynchronous setting is undecidable. To cope with this negative result, the only approaches we are aware of either restrict the syntax of session types or limit communication (by considering forms of bounded asynchrony). Both approaches are too restrictive in practice, hence we proceed differently by presenting an algorithm for checking subtyping which is sound, but not complete (in some cases it terminates without returning a decisive verdict). The algorithm is based on a tree representation of the coinductive definition of asynchronous subtyping; this tree could be infinite, and the algorithm checks for the presence of finite witnesses of infinite successful subtrees. Furthermore, we provide a tool that implements our algorithm. We use this tool to test our algorithm on many examples that cannot be managed with the previous approaches, and to provide an empirical evaluation of the time and space cost of the algorithm.
Miu A, Ferreira Ruiz F, Yoshida N, et al., 2021, Communication-safe web programming in TypeScript with routed multiparty session types, The International Conference on Compiler Construction (CC), Publisher: ACM, Pages: 94-106
Modern web programming involves coordinating interactions between browser clients and a server. Typically, the interactions in web-based distributed systems are informally described, making it hard to ensure correctness, especially communication safety, i.e. all endpoints progress without type errors or deadlocks, conforming to a specified protocol.We present STScript, a toolchain that generates TypeScript APIs for communication-safe web development over WebSockets, and RouST, a new session type theory that supports multiparty communications with routing mechanisms. STScript provides developers with TypeScript APIs generated from a communication protocol specification based on RouST. The generated APIs build upon TypeScript concurrency practices, complement the event-driven style of programming in full-stack web development, and are compatible with the Node.js runtime for server-side endpoints and the React.js framework for browser-side endpoints.RouST can express multiparty interactions routed via an intermediate participant. It supports peer-to-peer communication between browser-side endpoints by routing communication via the server in a way that avoids excessive serialisation. RouST guarantees communication safety for endpoint web applications written using STScript APIs.We evaluate the expressiveness of STScript for modern web programming using several production-ready case studies deployed as web applications.
Miu A, Ferreira F, Yoshida N, et al., 2021, Communication-Safe Web Programming in TypeScript with Routed Multiparty Session Types
Please refer to the README on https://github.com/STScript-2020/cc21-artifact/blob/main/README.md
This data is extracted from the Web of Science and reproduced under a licence from Thomson Reuters. You may not copy or re-distribute this data in whole or in part without the written consent of the Science business of Thomson Reuters.