检索结果-内蒙古大学图书馆

HasChor: Functional choreographic programming for All (Functional Pearl)

PROCEEDINGS OF THE ACM ON programming LANGUAGES-PACMPL 2023年第ICFP期7卷 541–565页

作者： Shen, Gan Kashiwa, Shun Kuper, Lindsey Univ Calif Santa Cruz Santa Cruz CA 95064 USA

choreographic programming is an emerging paradigm for programming distributed systems. In choreographic programming, the programmer describes the behavior of the entire system as a single, unified program - a choreography - which is then compiled to individual programs that run on each node, via a compilation step called endpoint projection. We present a new model for functional choreographic programming where choreographies are expressed as computations in a monad. Our model supports cutting-edge choreographic programming features that enable modularity and code reuse: in particular, it supports higher-order choreographies, in which a choreography may be passed as an argument to another choreography, and location-polymorphic choreographies, in which a choreography can abstract over nodes. Our model is implemented in a Haskell library, HasChor, which lets programmers write choreographic programs while using the rich Haskell ecosystem at no cost, bringing choreographic programming within reach of everyday Haskellers. Moreover, thanks to Haskell's abstractions, the implementation of the HasChor library itself is concise and understandable, boiling down endpoint projection to its short and simple essence.

关键词： choreographic programming freer monads

来源：评论

学校读者我要写书评

暂无评论

A model for correlation-based choreographic programming

引用

PEERJ COMPUTER SCIENCE 2024年 10卷 e1907-e1907页

作者： Giallorenzo, Saverio Montesi, Fabrizio Gabbrielli, Maurizio INRIA Sophia Antipolis France Univ Bologna Dept Comp Sci & Engn Bologna Italy Univ Southern Denmark Dept Math & Comp Sci Odense Denmark

Choreographies provide a clear way to specify the intended communication behaviour of concurrent and distributed systems. Previous theoretical work investigated the translation of choreographies into (models of) programs based on message passing. However, existing theories still present a gap between how they model communications-using channel names & agrave;la CCS or p-calculus-and implementations-which use lower-level mechanisms for message routing. We start bridging this gap with a new formal framework called Applied Choreographies. In Applied Choreographies, developers write choreographies in a familiar syntax (from previous work) and reason about their behaviour through simple, abstract name-based communication semantics. The framework offers state-of-the-art features of choreographic models, e.g., modular programming supported via choreographic types. To provide its correctness guarantee, Applied Choreographies comes with a compilation procedure that transforms a choreography into a low-level, implementation-adherent calculus of Service-Oriented Computing (SOC). To manage the complexity of the compilation, we divide its formalisation and proof into three stages, respectively dealing with: (a) the translation of name-based communications into their SOC equivalents, namely, using correlation mechanisms based on message data;(b) the projection of the given choreography into a composition of partial, single-participant choreographies (towards their translation into SOC processes);(c) the translation of partial choreographies and the distribution of global, choreography-level state into local SOC processes. We provide behavioural correspondence results for each stage. Thus, given a choreography specification, we guarantee to synthesise its faithful service-oriented implementation.

关键词： Concurrency Distributed programming Service-oriented computing choreographic programming

来源：评论

学校读者我要写书评

暂无评论

A Formal Theory of choreographic programming

引用

JOURNAL OF AUTOMATED REASONING 2023年第2期67卷 21-21页

作者： Cruz-Filipe, Luis Montesi, Fabrizio Peressotti, Marco Univ Southern Denmark Dept Math & Comp Sci Campusvej 55 DK-5230 Odense M Denmark

choreographic programming is a paradigm for writing coordination plans for distributed systems from a global point of view, from which correct-by-construction decentralised implementations can be generated automatically. Theory of choreographies typically includes a number of complex results that are proved by structural induction. The high number of cases and the subtle details in some of these proofs has led to important errors being found in published works. In this work, we formalise the theory of a choreographic programming language in Coq. Our development includes the basic properties of this language, a proof of its Turing completeness, a compilation procedure to a process language, and an operational characterisation of the correctness of this procedure. Our formalisation experience illustrates the benefits of using a theorem prover: we get both an additional degree of confidence from the mechanised proof, and a significant simplification of the underlying theory. Our results offer a foundation for the future formal development of choreographic languages.

关键词： choreographic programming Theorem proving Concurrency Process calculi

来源：评论

学校读者我要写书评

暂无评论

Choreography-Defined Networks: A Case Study on DoS Mitigation 22nd

Choreography-Defined Networks: A Case Study on DoS Mitigatio...

引用

22nd International Conference on Service Oriented Computing

作者： Giallorenzo, Saverio Mauro, Jacopo Melis, Andrea Montesi, Fabrizio Peressotti, Marco Prandini, Marco Univ Bologna Bologna Italy INRIA Sophia Antipolis France Univ Southern Denmark Odense Denmark

ISBN: (纸本)9789819608072;9789819608089

Software-defined networking and network function virtualization have brought unparalleled flexibility in defining and managing network architectures. With the widespread diffusion of cloud platforms, more resources are available to execute virtual network functions concurrently, but the current approach to defining networks in the cloud development is held back by the lack of tools to manage the composition of more complex flows than simple sequential invocations. In this paper, we advocate for the usage of choreographic programming for defining the multiparty workflows of a network. When applied to the composition of virtual network functions, this approach yields multiple advantages: a single program expresses the behavior of all components, in a way that is easier to understand and check;a compiler can produce the executable code for each component, guaranteeing correctness properties of their interactions such as deadlock freedom;and the bottleneck of a central orchestrator is removed. We describe the proposed approach and show its feasibility via a case study where different functions cooperatively solve a security monitoring task.

关键词： Software-defined Networks Virtual Network Functions choreographic programming Network Security Denial-of-Service

来源：评论

学校读者我要写书评

暂无评论

Certifying Choreography Compilation 1

引用

18th International Colloquium on Theoretical Aspects of Computing (ICTAC)

作者： Cruz-Filipe, Luis Montesi, Fabrizio Peressotti, Marco Univ Southern Denmark Dept Math & Comp Sci Campusvej 55 DK-5230 Odense M Denmark

ISBN: (数字)9783030853150

ISBN: (纸本)9783030853150;9783030853143

choreographic programming is a paradigm for developing concurrent and distributed systems, where programs are choreographies that define, from a global viewpoint, the computations and interactions that communicating processes should enact. Choreography compilation translates choreographies into the local definitions of process behaviours, given as terms in a process calculus. Proving choreography compilation correct is challenging and error-prone, because it requires relating languages in different paradigms (global interactions vs local actions) and dealing with a combinatorial explosion of proof cases. We present the first certified program for choreography compilation for a nontrivial choreographic language supporting recursion.

关键词： choreographic programming Formalisation Compilation

来源：评论

学校读者我要写书评

暂无评论

Certified Compilation of Choreographies with hacc 43rd

Certified Compilation of Choreographies with hacc

引用

43rd International Conference on Formal Techniques for Distributed Objects, Components and Systems (FORTE)

作者： Cruz-Filipe, Luis Lugovic, Lovro Montesi, Fabrizio Univ Southern Denmark Dept Math & Comp Sci Odense Denmark

ISBN: (纸本)9783031353543;9783031353550

programming communicating processes is challenging, because it requires writing separate programs that perform compatible send and receive actions at the right time during execution. Leaving this task to the programmer can easily lead to bugs. choreographic programming addresses this challenge by equipping developers with high-level abstractions for codifying the desired communication structures from a global viewpoint. Given a choreography, implementations of the involved processes can be automatically generated by endpoint projection (EPP). While choreographic programming prevents manual mistakes in the implementation of communications, the correctness of a choreographic programming framework crucially hinges on the correctness of its complex compiler, which has motivated formalisation of theories of choreographic programming in theorem provers. In this paper, we build upon one of these formalisations to construct a toolchain that produces executable code from a choreography.

关键词： choreographic programming Certified compilation Jolie Formal verification

来源：评论

学校读者我要写书评

暂无评论

Welcome to the Parti(tioning) (Functional Pearl) Using Rewrite Rules and Specialisation to Partition Haskell Programs 17

Welcome to the Parti(tioning) (Functional Pearl) Using Rewri...

引用

17th International Symposium on Haskell (Haskell)

作者： Krook, Robert Hammersberg, Samuel Chalmers Univ Technol Gothenburg Sweden Gothenburg Univ Gothenburg Sweden

ISBN: (纸本)9798400711022

Writing distributed applications is hard, as the programmer needs to describe the communication protocol between the different endpoints. If this is not done correctly, we can introduce bugs such as deadlocks and data races. Tierless and choreographic programming models aim to make this easier by describing the interactions of every endpoint in a single compilation unit. When such a program is compiled, ideally, a single endpoint is projected and the code for the other endpoints is removed. This leads to smaller binaries with fewer dependencies, and is called program partitioning. In this pearl, we show how we can use rewrite rules and specialisation to get GHC to partition our Haskell programs (almost) for free, if they are written using the Haste App or HasChor framework. As an example of why partitioning is useful, we show how an example application can be more easily built and deployed after being partitioned.

关键词： Haskell Program Partitioning choreographic programming Tierless programming Specialisation Rewrite Rules

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：