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

23rd International Conference on Coordination Models and Language (COORDINATION)

作者： Saffrich, Hannes Thiemann, Peter Univ Freiburg Freiburg Germany

ISBN: (纸本)9783030781415;9783030781422

Imperative session types provide an imperative interface to session-typed communication in a functional language. Compared to functional session type APIs, the program structure is simpler at the surface, but typestate is required to model the current state of communication throughout. Most work on session types has neglected the imperative approach. We demonstrate that the functional approach subsumes previous work on imperative session types by exhibiting a typing and semantics preserving translation into a system of linear functional session types. We further show that the untyped backwards translation from the functional to the imperative calculus is semantics preserving. We restrict the type system of the functional calculus such that the backwards translation becomes type preserving. Thus, we precisely capture the difference in expressiveness of the two calculi and conclude that the lack of expressiveness in the imperative calculus is solely due to its type system.

关键词： Session types distributed programming Translation

来源：评论

学校读者我要写书评

暂无评论

Communicating Finite State Machines and an Extensible Toolchain for Multiparty Session Types 23rd

Communicating Finite State Machines and an Extensible Toolch...

引用

23rd International Symposium on Fundamentals of Computation Theory (FCT)

作者： Yoshida, Nobuko Zhou, Fangyi Ferreira, Francisco Imperial Coll London London England

ISBN: (纸本)9783030865931;9783030865924

Multiparty session types (MPST) provide a typing discipline for message passing concurrency, ensuring deadlock freedom for distributed processes. This paper first summarises the relationship between MPST and communicating finite state machines (CFSMs), which offers not only theoretical justifications of MPST but also a guidance to implement MPST in practice. As one of the applications, we present vSCR (NuScR), an extensible toolchain for MPST-based multiparty protocols. The toolchain can convert multiparty protocols in the SCRIBBLE protocol description language into global types in the MPST theory;global types are projected into local types, and local types are converted to their corresponding CFSMs. The toolchain also generates APIs from CFSMs that implement endpoints in the protocol. Our design allows for language-independent code generation, and opens possibilities to generate APIs in various programming languages. We design our toolchain with modularity and extensibility in mind, so that extensions of core MPST can be easily integrated within our framework. As a case study, we show the implementation of the nested protocol extension in vScR, to showcase our extensibility.

关键词： Session Types Communicating Finite State Machines distributed programming Scribble Protocols

来源：评论

学校读者我要写书评

暂无评论

Foundations of Consistency Types for a Higher-Order distributed Language 1

引用

32nd International Workshop on Languages and Compilers for Parallel Computing (LCPC)

作者： Zhao, Xin Haller, Philipp KTH Royal Inst Technol Stockholm Sweden

ISBN: (数字)9783030727895

ISBN: (纸本)9783030727895;9783030727888

distributed systems address the increasing demand for fast access to resources and fault tolerance for data. However, due to scalability requirements, software developers need to trade consistency for performance. For certain data, consistency guarantees may be weakened if application correctness is unaffected. In contrast, data flow from data with weak consistency to data with strong consistency requirements is problematic, since application correctness may be broken. In this paper, we propose LCD, a higher-order static consistency-typed language with replicated data types. The type system of LCD statically enforces noninterference between data types with weak consistency and data types with strong consistency. This means that updates of weakly-consistent data can never affect strongly-consistent data. Finally, our main theorem guarantees sequential consistency for so-called con operations in our language.

关键词： Consistency types Type system distributed programming

来源：评论

学校读者我要写书评

暂无评论

A Subtyping Scheme for Nominal and Structural Types Based on Class Graph Equivalence 4

A Subtyping Scheme for Nominal and Structural Types Based on...

引用

4th International Conference on Blockchain Technology and Applications (ICBTA)

作者： Ke, Wei Chan, Ka-Hou Macao Polytech Inst Sch Appl Sci Macau Peoples R China

ISBN: (纸本)9781450387460

Subtyping and multiple inheritance are the essential features of oo and component-based programming languages, in particular with the presence of interfaces and contracts. More general, the composability of these constructs admitting the subtype relation powers the reusability, modular, flexibility and reliability of oo-based systems. While nominal classes allow annotation of user intention to the types, operations on interfaces and contracts naturally result structural constructs. Structural types are also necessary if we need the types to have value-semantics, so that they can be transferred around in distributed systems. Building a type system that allows the coexistence of nominal and structural classes, while maintaining the usual subtype relation is critical and challenging. We present a subtyping scheme that encodes a class to a directed and edge-labeled graph, which has the convenience to handle recursive types. The names of a class and its superclasses are encoded as tags to label the edges of the graph, turning the nominal construct into a structural one. This encoding allows us to unify the handling of class relations into graph relations. We define the class representation, canonical form, value-identity and subtype relation in the notion of graphs, and justify our subtyping scheme in the cases of multiple inheritance, class intersection and union. Our scheme is general, easy to implement and compatible with most of the existing oo type systems, providing a solid base for further oo language and tool development.

关键词： subtyping nominal subtyping structural subtyping multiple inheritance intersection type union type class graph recursive type type equivalence object-oriented language distributed programming

来源：评论

学校读者我要写书评

暂无评论

Parallel distributed productivity-aware tree-search using Chapel

引用

CONCURRENCY AND COMPUTATION-PRACTICE & EXPERIENCE 2023年第27期35卷

作者： Helbecque, Guillaume Gmys, Jan Melab, Nouredine Carneiro, Tiago Bouvry, Pascal Univ Lille Ctr Inria Univ Lille CNRS CRIStAL UMR 9189 Lille France Univ Luxembourg FSTM Luxembourg City Luxembourg Univ Luxembourg DCS FSTM SnT Luxembourg City Luxembourg

With the recent arrival of the exascale era, modern supercomputers are increasingly big making their programming much more complex. In addition to performance, software productivity is a major concern to choose a programming language, such as Chapel, designed for exascale computing. In this paper, we investigate the design of a parallel distributed tree-search algorithm, namely P3D-DFS, and its implementation using Chapel. The design is based on the Chapel's DistBag data structure, revisited by: (1) redefining the data structure for Depth-First tree-Search (DFS), henceforth renamed DistBag-DFS;(2) redesigning the underlying load balancing mechanism. In addition, we propose two instantiations of P3D-DFS considering the Branch-and-Bound (B & B) and Unbalanced Tree Search (UTS) algorithms. In order to evaluate how much performance is traded for productivity, we compare the Chapel-based implementations of B & B and UTS to their best-known counterparts based on traditional OpenMP (intra-node) and MPI+X (inter-node). For experimental validation using 4096 processing cores, we consider the permutation flow-shop scheduling problem for B & B and synthetic literature benchmarks for UTS. The reported results show that P3D-DFS competes with its OpenMP baselines for coarser-grained shared-memory scenarios, and with its MPI+X counterparts for distributed-memory settings, considering both performance and productivity-awareness. In the context of this work, this makes Chapel an alternative to OpenMP/MPI+X for exascale programming.

关键词： Branch-and-Bound Chapel distributed programming productivity-awareness unbalanced tree-search

来源：评论

学校读者我要写书评

暂无评论

Concurrent and distributed Pseudocode: A Systematic Literature Review 47

Concurrent and Distributed Pseudocode: A Systematic Literatu...

引用

47th Latin American Computing Conference (CLEI)

作者： Ulate-Caballero, Bryan Alexander Berrocal-Rojas, Allan Hidalgo-Cespedes, Jeisson Univ Costa Rica Comp & Informat San Jose Costa Rica Univ Costa Rica ECCI San Jose Costa Rica Univ Costa Rica ECCI CITIC San Jose Costa Rica

ISBN: (纸本)9781665495035

Pseudocode is a valuable resource used in programming education, software development, and scientific reports for designing algorithmic solutions as it is easy to write, understand, and modify. Since pseudocode is lacking in its ability to be tested, it is difficult to determine whether a pseudocode solution is correct or not. Software tools are specially required to reach this goal, e.g., helping professors find race conditions, deadlocks, or starvation issues while grading students' concurrent pseudocode. Although there are various tools to work with sequential pseudocode, there is a lack of tools to work with concurrent pseudocode. This shortage motivated us to determine the state-of-the-art in notations and tools for testing concurrent and distributed pseudocode. We conducted a systematic literature review and found only a few related publications, confirming that this topic is understudied. We found and report about five software tools capable of interpreting concurrent or distributed pseudocode, and two software tools capable of verifying its correctness. As another result, no other literature review was found about this topic, conferring novelty to the contributions of this work.

关键词： Concurrent pseudocode distributed pseudocode parallel pseudocode code correctness concurrent programming distributed programming parallel programming pseudocode pseudo-code pseudo-language education teaching

来源：评论

学校读者我要写书评

暂无评论

Replicated data types that unify eventual consistency and observable atomic consistency

引用

JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN programming 2020年 114卷

作者： Zhao, Xin Haller, Philipp KTH Royal Inst Technol Sch Elect Engn & Comp Sci SE-10044 Stockholm Sweden

Strong consistency is widely used in systems such as relational databases. In a distributed system, strong consistency ensures that all clients observe consistent data updates atomically on all servers. However, such systems need to sacrifice availability when synchronization occurs. We propose a new consistency protocol, the observable atomic consistency protocol (OACP) to make write-dominant applications as fast as possible and as consistent as needed. OACP combines the advantages of (1) mergeable data types, specifically, convergent replicated data types, to reduce synchronization and (2) reliable total order broadcast to provide on-demand strong consistency. We also provide a high-level programming interface to improve the efficiency and correctness of distributed programming. We present a formal, mechanized model of OACP in rewriting logic and verify key correctness properties using the model checking tool Maude. Furthermore, we provide a prototype implementation of OACP based on Akka, a widely-used actor-based middleware. Our experimental evaluation shows that OACP can reduce coordination overhead compared to the state-of-the-art Raft consensus protocol. Our results also suggest that OACP increases availability through mergeable data types and provides acceptable latency for achieving strong consistency, enabling a principled relaxation of strong consistency to improve performance. (C) 2020 The Authors. Published by Elsevier Inc.

关键词： Atomic consistency Eventual consistency CRDT Actor model distributed programming

来源：评论

学校读者我要写书评

暂无评论

DisGCo: A Compiler for distributed Graph Analytics

引用

ACM TRANSACTIONS ON ARCHITECTURE AND CODE OPTIMIZATION 2020年第4期17卷 1–26页

作者： Rajendran, Anchu Nandivada, V. Krishna Indian Inst Technol Madras Chennai Tamil Nadu India IIT Madras Dept CSE Chennai 600036 Tamil Nadu India

Graph algorithms are widely used in various applications. Their programmability and performance have garnered a lot of interest among the researchers. Being able to run these graph analytics programs on distributed systems is an important requirement. Green-Marl is a popular Domain Specific Language (DSL) for coding graph algorithms and is known for its simplicity. However, the existing Green-Marl compiler for distributed systems (Green-Marl to Pregel) can only compile limited types of Green-Marl programs (in Pregel canonical form). This severely restricts the types of parallel Green-Marl programs that can be executed on distributed systems. We present DisGCo, the first compiler to translate any general Green-Marl program to equivalent MPI program that can run on distributed systems. Translating Green-Marl programs to MPI (SPMD/MPMD style of computation, distributed memory) presents many other exciting challenges, besides the issues related to differences in syntax, as Green-Marl gives the programmer a unified view of the whole memory and allows the parallel and serial code to be intermixed. We first present the set of challenges involved in translating Green-Marl programs to MPI and then present a systematic approach to do the translation. We also present a few optimization techniques to improve the performance of our generated programs. DisGCo is the first graph DSL compiler that can handle all syntactic capabilities of a practical graph DSL like Green-Marl and generate code that can run on distributed systems. Our preliminary evaluation of DisGCo shows that our generated programs are scalable. Further, compared to the state-of-the-art DH-Falcon compiler that translates a subset of Falcon programs to MPI, our generated codes exhibit a geomean speedup of 17.32x.

关键词： Graph analytics distributed programming GreenMarl

来源：评论

学校读者我要写书评

暂无评论

A Subtyping Scheme for Nominal and Structural Types Based on Class Graph Equivalence 2021

A Subtyping Scheme for Nominal and Structural Types Based on...

引用

2021 4th International Conference on Blockchain Technology and Applications

作者： Wei Ke Ka-Hou Chan School of Applied Sciences Macao Polytechnic Institute Macao

ISBN: (纸本)9781450387460

关键词： nominal subtyping recursive type class graph type equivalence intersection type distributed programming structural subtyping union type object-oriented language subtyping multiple inheritance

来源：评论

学校读者我要写书评

暂无评论

Statically Verified Refinements for Multiparty Protocols

引用

PROCEEDINGS OF THE ACM ON programming LANGUAGES-PACMPL 2020年第OOPSLA期4卷 1–30页

作者： Zhou, Fangyi Ferreira, Francisco Hu, Raymond Neykova, Rumyana Yoshida, Nobuko Imperial Coll London London England Univ Hertfordshire Hatfield Herts England Brunel Univ London London England

With distributed computing becoming ubiquitous in the modern era, safe distributed programming is an open challenge. To address this, multiparty session types (MPST) provide a typing discipline for message-passing concurrency, guaranteeing communication safety properties such as deadlock freedom. While originally MPST focus on the communication aspects, and employ a simple typing system for communication payloads, communication protocols in the real world usually contain constraints on the payload. We introduce refined multiparty session types (RMPST), an extension of MPST, that express data dependent protocols via refinement types on the data types. We provide an implementation of RMPST, in a toolchain called SESSION * , using SCRIBBLE, a toolchain for multiparty protocols, and targeting F*, a verification-oriented functional programming language. Users can describe a protocol in SCRIBBLE and implement the endpoints in F* using refinement-typed APIs generated from the protocol. The F* compiler can then statically verify the refinements. Moreover, we use a novel approach of callback-styled API generation, providing static linearity guarantees with the inversion of control. We evaluate our approach with real world examples and show that it has little overhead compared to a naive implementation, while guaranteeing safety properties from the underlying theory.

关键词： Multiparty Session Types (MPST) Refinement Types Code Generation F distributed programming

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：