scholarly journals Gobra: Modular Specification and Verification of Go Programs

2021 ◽  
pp. 367-379
Author(s):  
Felix A. Wolf ◽  
Linard Arquint ◽  
Martin Clochard ◽  
Wytse Oortwijn ◽  
João C. Pereira ◽  
...  
Keyword(s):  
Distributed Systems ◽  
Programming Language ◽  
Message Passing ◽  
Safety Data ◽  
Separation Logic ◽  
Data Race ◽  
Static Verification ◽  
Crash Safety ◽  
Concurrent And Distributed Systems ◽  
Systems Programming

AbstractGo is an increasingly-popular systems programming language targeting, especially, concurrent and distributed systems. Go differentiates itself from other imperative languages by offering structural subtyping and lightweight concurrency through goroutines with message-passing communication. This combination of features poses interesting challenges for static verification, most prominently the combination of a mutable heap and advanced concurrency primitives.We present Gobra, a modular, deductive program verifier for Go that proves memory safety, crash safety, data-race freedom, and user-provided specifications. Gobra is based on separation logic and supports a large subset of Go. Its implementation translates an annotated Go program into the Viper intermediate verification language and uses an existing SMT-based verification backend to compute and discharge proof obligations.

scholarly journals Defining a general object model of distributed systems entities in Java

2003 ◽  
Vol 16 (2) ◽  
pp. 185-194
Author(s):  
Nenad Jovanovic ◽  
Ranko Popovic ◽  
Zoran Jovanovic
Keyword(s):  
Distributed Systems ◽  
Programming Language ◽  
Message Passing ◽  
Present Model ◽  
Heterogeneous Systems ◽  
Object Model ◽  
Java Programming ◽  
Xml Document ◽  
General Object ◽  
Model Components

This paper deals with modeling and simulation of distributed systems in Java programming language. Distributed systems consist of components which communicate and coordinate their actions by passing messages. Components of distributed systems which define some functionality are entities determined with static attributes. The paper presents general model for modeling in Java environment entities distributed systems communicate using message passing protocol. We described a way to present model components and their functional links in a form of an XML document. A model can be executed as an application and (or) an applet. Presented model can be used for modeling heterogeneous systems.

The NIL distributed systems programming language

1985 ◽  
Vol 20 (5) ◽  
pp. 36-44 ◽  
Author(s):  
Rob Strom ◽  
Shaula Yemini
Keyword(s):  
Distributed Systems ◽  
Programming Language ◽  
Systems Programming

scholarly journals Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems

2020 ◽  
pp. 336-365 ◽  
Author(s):  
Morten Krogh-Jespersen ◽  
Amin Timany ◽  
Marit Edna Ohlenbusch ◽  
Simon Oddershede Gregersen ◽  
Lars Birkedal
Keyword(s):  
Distributed Systems ◽  
Higher Order ◽  
Separation Logic ◽  
Two Phase ◽  
Modular Reasoning ◽  
Multiple Servers ◽  
Local Reasoning ◽  
Load Balancer ◽  
Concurrent And Distributed Systems ◽  
Great Complexity

AbstractBuilding network-connected programs and distributed systems is a powerful way to provide scalability and availability in a digital, always-connected era. However, with great power comes great complexity. Reasoning about distributed systems is well-known to be difficult. In this paper we present , a novel framework based on separation logic supporting modular, node-local reasoning about concurrent and distributed systems. The logic is higher-order, concurrent, with higher-order store and network sockets, and is fully mechanized in the Coq proof assistant. We use our framework to verify an implementation of a load balancer that uses multi-threading to distribute load amongst multiple servers and an implementation of the two-phase-commit protocol with a replicated logging service as a client. The two examples certify that is well-suited for both horizontal and vertical modular reasoning.

Causal-Consistent Replay Reversible Semantics for Message Passing Concurrent Programs

2021 ◽  
Vol 178 (3) ◽  
pp. 229-266
Author(s):  
Ivan Lanese ◽  
Adrián Palacios ◽  
Germán Vidal
Keyword(s):  
Programming Language ◽  
Message Passing ◽  
Concurrent Programming ◽  
Concurrent Systems ◽  
Concurrent Programs ◽  
Unified Framework ◽  
Innovative Technique ◽  
Dual Notion

Causal-consistent reversible debugging is an innovative technique for debugging concurrent systems. It allows one to go back in the execution focusing on the actions that most likely caused a visible misbehavior. When such an action is selected, the debugger undoes it, including all and only its consequences. This operation is called a causal-consistent rollback. In this way, the user can avoid being distracted by the actions of other, unrelated processes. In this work, we introduce its dual notion: causal-consistent replay. We allow the user to record an execution of a running program and, in contrast to traditional replay debuggers, to reproduce a visible misbehavior inside the debugger including all and only its causes. Furthermore, we present a unified framework that combines both causal-consistent replay and causal-consistent rollback. Although most of the ideas that we present are rather general, we focus on a popular functional and concurrent programming language based on message passing: Erlang.

scholarly journals Distributed Singular Value Decomposition Method for Fast Data Processing in Recommendation Systems

Energies ◽  
2021 ◽  
Vol 14 (8) ◽  
pp. 2284
Author(s):  
Krzysztof Przystupa ◽  
Mykola Beshley ◽  
Olena Hordiichuk-Bublivska ◽  
Marian Kyryk ◽  
Halyna Beshley ◽  
...  
Keyword(s):  
Distributed Systems ◽  
Singular Value Decomposition ◽  
Data Processing ◽  
Message Passing ◽  
Message Passing Interface ◽  
Recommendation Systems ◽  
Singular Value ◽  
Singular Value Decomposition Method ◽  
Value Decomposition ◽  
Svd Method

The problem of analyzing a big amount of user data to determine their preferences and, based on these data, to provide recommendations on new products is important. Depending on the correctness and timeliness of the recommendations, significant profits or losses can be obtained. The task of analyzing data on users of services of companies is carried out in special recommendation systems. However, with a large number of users, the data for processing become very big, which causes complexity in the work of recommendation systems. For efficient data analysis in commercial systems, the Singular Value Decomposition (SVD) method can perform intelligent analysis of information. With a large amount of processed information we proposed to use distributed systems. This approach allows reducing time of data processing and recommendations to users. For the experimental study, we implemented the distributed SVD method using Message Passing Interface, Hadoop and Spark technologies and obtained the results of reducing the time of data processing when using distributed systems compared to non-distributed ones.

scholarly journals The Emulated OCODE Machine for the Support of BCPL

1975 ◽  
Vol 4 (45) ◽  
Author(s):  
Ole Sørensen
Keyword(s):  
Operating System ◽  
Programming Language ◽  
Design Process ◽  
Internal Representation ◽  
The Past ◽  
Future Analysis ◽  
Systems Programming

In the spring of 1973 it was decided to implement the language BCPL on the experimental microprogrammable computer RIKKE-1 being constructed in this department. The language was chosen to be the systems programming language for RlKKE-1, one argurment being the possibility of transferring the Oxford Operating system OS 8 to RIKKE-1. This paper describes the design process for an internal representation of OCODE, the resulting machine, the emulator, and the assembler, and finally there is a discussion of our experiences of running the OCODE machine during the past 8 months. Some future analysis and possible modifications are mentioned.

Sign in / Sign up

Export Citation Format

Share Document