The proposed framework provides a general model of concurrent imperative programming. Programs are modeled as formal languages and concurrency as an interleaving (or shuffle) operator. This yields a simple and elegant algebra of programs. The framework supports the views program logic by Dinsdale-Young and others, which generalizes various type systems and separation logic approaches to program correctness. It also validates familiar operational calculi in small-step and big-step flavours. The consistency of the program logic with respect to the operational rules is established directly and does not use induction on derivations. In fact the whole framework uses only straightforward mathematics. Parametric in states, views and basic commands, it can be instantiated to a variety of concrete languages and settings.
We introduce a method of reversing the execution of imperative concurrent programs. Given an irreversible program, we describe the process of producing two versions. The first performs forward execution and saves information necessary for reversal. The second uses this saved information to simulate reversal. We propose using identifiers to overcome challenges of reversing concurrent programs. We prove this reversibility to be correct, showing that the initial program state is restored and that all saved information is used (garbage-free).
We propose a new concurrent model for imperative languages where concurrency occurs at a subprogram level. This model introduces a new {\it block sequential} statement of the form $#(G_1,\ldots,G_n)$ where each $G_i$ is a statement. This statement tells the machine to execute $G_1,\ldots,G_n$ sequentially and atomically (\ie, without interleaving). It therefore enhances atomicity and predictability in concurrent programming. We illustrate our idea via $C^{\|}$, an extension of the core concurrent C with the new block sequential statement.
The aim of the Alma project is the design of a strongly typed constraint programming language that combines the advantages of logic and imperative programming. The first stage of the project was the design and implementation of Alma-0, a small programming language that provides a support for declarative programming within the imperative programming framework. It is obtained by extending a subset of Modula-2 by a small number of features inspired by the logic programming paradigm. In this paper we discuss the rationale for the design of Alma-0, the benefits of the resulting hybrid programming f…
In (Apt et al, TOPLAS 1998) we introduced the imperative programming language Alma-0 that supports declarative programming. In this paper we illustrate the hybrid programming style of Alma-0 by means of various examples that complement those presented in (Apt et al, TOPLAS 1998). The presented Alma-0 programs illustrate the versatility of the language and show that ``don't know'' nondeterminism can be naturally combined with assignment.
The ramification method in Implicit Computational Complexity has been associated with functional programming, but adapting it to generic imperative programming is highly desirable, given the wider algorithmic applicability of imperative programming. We introduce a new approach to ramification which, among other benefits, adapts readily to fully general imperative programming. The novelty is in ramifying finite second-order objects, namely finite structures, rather than ramifying elements of free algebras. In so doing we bridge between Implicit Complexity's type theoretic characterizations of f…
We describe a type system for a platform called the General Intensional Programming System (GIPSY), designed to support intensional programming languages built upon intensional logic and their imperative counter-parts for the intensional execution model. In GIPSY, the type system glues the static and dynamic typing between intensional and imperative languages in its compiler and run-time environments to support the intensional evaluation of expressions written in various dialects of the intensional programming language Lucid. The intensionality makes expressions to explicitly take into the acc…
In machine learning (ML), researchers and engineers seem to be at odds. System implementers would prefer models to be declarative, with detailed type information and semantic restrictions that allow models to be optimised, rearranged and parallelised. Yet practitioners show an overwhelming preference for dynamic, imperative languages with mutable state, and much engineering effort is spent bridging the resulting semantic divide. Is there a fundamental conflict? This article explores why imperative and functional styles are used, and how future language designs might get the best of both worlds…
Term rewriting systems have a simple syntax and semantics and facilitate proofs of correctness. However, they are not as popular in industry or academia as imperative languages. We define a term rewriting based abstract programming language with an imperative style and a precise semantics allowing programs to be translatable into efficient imperative languages, to obtain proofs of correctness together with efficient execution. This language is designed to facilitate translations into correct programs in imperative languages with assignment statements, iteration, recursion, arrays, pointers, an…
To deal with failures as simply as possible, we propose a new foun- dation for the core (untyped) C, which is based on a new logic called task logic or imperative logic. We then introduce a sequential-disjunctive statement of the form S : R. This statement has the following semantics: execute S and R sequentially. It is considered a success if at least one of S;R is a success. This statement is useful for dealing with inessential errors without explicitly catching them.
One of the most recent architectures of networks is Software-Defined Networks (SDNs) using a con- troller appliance to control the set of switches on the network. The controlling process includes installing or uninstalling packet-processing rules on flow tables of switches. This paper presents a high-level imperative network programming language, called ImNet, to facilitate writing efficient, yet simple, programs executed by controller to manage switches. ImNet is simply-structured, expressive, compositional, and imperative. This paper also introduces an operational semantics to ImNet. Detaile…
In this paper, we describe an IDE called CAPS (Calculational Assistant for Programming from Specifications) for the interactive, calculational derivation of imperative programs. In building CAPS, our aim has been to make the IDE accessible to non-experts while retaining the overall flavor of the pen-and-paper calculational style. We discuss the overall architecture of the CAPS system, the main features of the IDE, the GUI design, and the trade-offs involved.
We propose a novel, operational framework to formally describe the semantics of concurrent programs running within the context of a relaxed memory model. Our framework features a "temporary store" where the memory operations issued by the threads are recorded, in program order. A memory model then specifies the conditions under which a pending operation from this sequence is allowed to be globally performed, possibly out of order. The memory model also involves a "write grain," accounting for architectures where a thread may read a write that is not yet globally visible. Our formal model is su…
Adding versatile interactions to imperative programming -- C, Java and Android -- is an essential task. Unfortunately, existing languages provide only limited constructs for user interaction. These constructs are usually in the form of $unbounded$ quantification. For example, existing languages can take the keyboard input from the user only via the $read(x)/scan(x)$ construct. Note that the value of $x$ is unbounded in the sense that $x$ can have any value. This construct is thus not useful for applications with bounded inputs. To support bounded choices, we propose new bounded-choice statemen…
In this paper we present several examples of solving algorithmic problems from the Google Code Jam programming contest with Picat programming language using declarative techniques: constraint logic programming and tabled logic programming. In some cases the use of Picat simplifies the implementation compared to conventional imperative programming languages, while in others it allows to directly convert the problem statement into an efficiently solvable declarative problem specification without inventing an imperative algorithm.
In this paper, we bring anonymous variables into imperative languages. Anonymous variables represent don't-care values and have proven useful in logic programming. To bring the same level of benefits into imperative languages, we describe an extension to C wth anonymous variables.
Seoul National University（首尔大学）；FriendliAI；Samsung Research（三星研究院）；University of California, Berkeley（加州大学伯克利分校）
Imperative programming allows users to implement their deep neural networks (DNNs) easily and has become an essential part of recent deep learning (DL) frameworks. Recently, several systems have been proposed to combine the usability of imperative programming with the optimized performance of symbolic graph execution. Such systems convert imperative Python DL programs to optimized symbolic graphs and execute them. However, they cannot fully support the usability of imperative programming. For example, if an imperative DL program contains a Python feature with no corresponding symbolic represen…
We present a concurrent framework for Win32 programming based on Concurrent ML, a concurrent language with higher-order functions, static typing, lightweight threads and synchronous communication channels. The key points of the framework are the move from an event loop model to a threaded model for the processing of window messages, and the decoupling of controls notifications from the system messages. This last point allows us to derive a general way of writing controls that leads to easy composition, and can accommodate ActiveX Controls in a transparent way.
Selection statements -- if-then-else, switch and try-catch -- are commonly used in modern imperative programming languages. We propose another selection statement called a {\it choice existentially quantified statement}. This statement turns out to be quite useful for pattern matching among several merits. Examples will be provided for this statement.
We have designed a new logic programming language called LM (Linear Meld) for programming graph-based algorithms in a declarative fashion. Our language is based on linear logic, an expressive logical system where logical facts can be consumed. Because LM integrates both classical and linear logic, LM tends to be more expressive than other logic programming languages. LM programs are naturally concurrent because facts are partitioned by nodes of a graph data structure. Computation is performed at the node level while communication happens between connected nodes. In this paper, we present the s…
While event handling is a key element in modern interactive programming, it is unfortunate that its theoretical foundation is rather weak. To solve this problem, we propose to adopt a game-logical approach of computability logic \cite{Jap08} to event handling.
In this note we revisit the so-called reactive programming style, which evolves from the synchronous programming model of the Esterel language by weakening the assumption that the absence of an event can be detected instantaneously. We review some research directions that have been explored since the emergence of the reactive model ten years ago. We shall also outline some questions that remain to be investigated.
We report on intermediate results of our research on reasoning about liveness properties in addition to deep correctness properties for an imperative, concurrent programming language with a higher-order store. At present, we focus on one particular liveness property, namely termination. By guaranteeing termination we can strengthen statements of partial correctness to total correctness. This is achieved by the classic approach of turning termination into a safety property. In particular we extend the programming language under consideration with call permissions, which have been shown to enabl…
Pure Lucid programs are concurrent with very fine granularity. Sequential Threads (STs) are functions introduced to enlarge the grain size; they are passed from server to workers by Communication Procedures (CPs) in the General Intensional Programming System (GIPSY). A JLucid program combines Java code for the STs with Lucid code for parallel control. Thus first, in this thesis, we describe the way in which the new JLucid compiler generates STs and CPs. JLucid also introduces array support. Further exploration goes through the additional transformations that the Lucid family of languages has u…
Dataflow languages provide natural support for specifying constraints between objects in dynamic applications, where programs need to react efficiently to changes of their environment. Researchers have long investigated how to take advantage of dataflow constraints by embedding them into procedural languages. Previous mixed imperative/dataflow systems, however, require syntactic extensions or libraries of ad hoc data types for binding the imperative program to the dataflow solver. In this paper we propose a novel approach that smoothly combines the two paradigms without placing undue burden on…
Rust is a popular programming language in building various low-level software in recent years. It aims to provide safe concurrency when implementing multi-threaded software through a suite of compiler checking rules. Unfortunately, there is limited understanding of how the checking rules influence the safety of concurrent programming in Rust applications. In this paper, we perform a preliminary study on Rust's concurrency safety from two aspects: concurrency usage and concurrency bugs. Our study can provide better understanding on Rust's concurrency and can guide future researchers and practit…
Concurrent separation logic (CSL) is a specification logic for concurrent imperative programs with shared memory and locks. In this paper, we develop a concurrent and interactive account of the logic inspired by asynchronous game semantics. To every program $C$, we associate a pair of asynchronous transition systems $[C]_S$ and $[C]_L$ which describe the operational behavior of the Code when confronted to its Environment or Frame --- both at the level of machine states ($S$) and of machine instructions and locks ($L$). We then establish that every derivation tree $π$ of a judgment $Γ\vdash\{P\…
In functional programming, point-free relation calculi have been fruitful for general theories of program construction, but for specific applications pointwise expressions can be more convenient and comprehensible. In imperative programming, refinement calculi have been tied to pointwise expression in terms of state variables, with the curious exception of the ubiquitous but invisible heap. To integrate pointwise with point-free, de Moor and Gibbons extended lambda calculus with non-injective pattern matching interpreted using relations. This article gives a semantics of that language using ``…
Declarative styles such as functional programming (FP) are rapidly gaining ground on their imperative cousins, including procedural and object-oriented programming. The shift is subtle because it is happening within the context of multiparadigm programming languages such as JavaScript. FP is better suited to modern processes like test-driven development (TDD), and architectures like massively parallel, cloud-based computing. This article describes the technical details that characterize the shift from imperative to FP and implications for software quality management, particularly reuse and tes…
In this paper we propose a new approach to the description of a network of interacting processes in a traditional programming language. Special programming languages or extensions to sequential languages are usually designed to express the semantics of concurrent execution. Using libraries in C++, Java, C#, and other languages is more practical way of concurrent programming. However, this method leads to an increase in workload of a manual coding. Besides, stock compilers can not detect semantic errors related to the programming model in such libraries. The new markup language and a special te…
We describe a generative approach that enables concurrent typestate-oriented programming in Java and other mainstream languages. The approach allows programmers to implement objects exposing a state-sensitive interface using a high-level synchronization abstraction that synchronizes methods with the states of the receiver object in which those methods have an effect. An external tool takes care of generating all the boilerplate code that implements the synchronization logic. Behavioral types are used to specify object protocols. The tool integrates protocol conformance verification with the sy…
We tackle the problem of automatically designing concurrent data structure operations given a sequential data structure specification and knowledge about concurrent behavior. Designing concurrent code is a non-trivial task even in simplest of cases. Humans often design concurrent data structure operations by transforming sequential versions into their respective concurrent versions. This requires an understanding of the data structure, its sequential behavior, thread interactions during concurrent execution and shared memory synchronization primitives. We mechanize this design process using au…
Hybrid systems, which combine discrete and continuous dynamics, require quality modeling languages to be either described or analyzed. The Concurrent Constraint paradigm (ccp) is an expressive declarative paradigm, characterized by the use of a common constraint store to communicate and synchronize concurrent agents. In this paradigm, the information is stated in the form of constraints, in contrast to the variable/value style typical of imperative languages. Several extensions of ccp have been proposed in order to model reactive systems. One of these extensions is the Timed Concurrent Constra…
This is a tutorial on logic programming and Prolog appropriate for a course on programming languages for students familiar with imperative programming.
Concurrency has been rapidly gaining importance in general-purpose computing, caused by the recent turn towards multicore processing architectures. As a result, an increasing number of developers have to learn to write concurrent programs, a task that is known to be hard even for the expert. Language designers are therefore working on languages that promise to make concurrent programming "easier" than using traditional thread libraries. However, the claim that a new language is more usable than another cannot be supported by purely theoretical considerations, but calls for empirical studies. I…
Software and hardware components are basic parts of modern networks. However the software compo- nent is typical sealed and function-oriented. Therefore it is very difficult to modify these components. This badly affected networking innovations. Moreover, this resulted in network policies having complex interfaces that are not user-friendly and hence resulted in huge and complicated flow tables on physical switches of networks. This greatly degrades the network performance in many cases. Software-Defined Networks (SDNs) is a modern architecture of networks to overcome issues mentioned above. T…
CalcuList (Calculator with List manipulation), is an educational language for teaching functional programming extended with some imperative and side-effect features, which are enabled under explicit request by the programmer. In addition to strings and lists, the language natively supports json objects. The language adopts a Python-like syntax and enables interactive computation sessions with the user through a REPL (Read-Evaluate-Print-Loop) shell. The object code produced by a compilation is a program that will be eventually executed by the CalcuList Virtual Machine (CLVM).
Reactive programs combine traditional sequential programming constructs with primitives to allow communication with other concurrent agents. They are ubiquitous in modern applications, ranging from components systems and web services, to cyber-physical systems and autonomous robots. In this paper, we present an algebraic verification strategy for concurrent reactive programs, with a large or infinite state space. We define novel operators to characterise interactions and state updates, and an associated equational theory. With this we can calculate a reactive program's denotational semantics, …
We present a novel algorithm that synthesizes imperative programs for introductory programming courses. Given a set of input-output examples and a partial program, our algorithm generates a complete program that is consistent with every example. Our key idea is to combine enumerative program synthesis and static analysis, which aggressively prunes out a large search space while guaranteeing to find, if any, a correct solution. We have implemented our algorithm in a tool, called SIMPL, and evaluated it on 30 problems used in introductory programming courses. The results show that SIMPL is able …
Formal, mathematically rigorous programming language semantics are the essential prerequisite for the design of logics and calculi that permit automated reasoning about concurrent programs. We propose a novel modular semantics designed to align smoothly with program logics used in deductive verification and formal specification of concurrent programs. Our semantics separates local evaluation of expressions and statements performed in an abstract, symbolic environment from their composition into global computations, at which point they are concretised. This makes incremental addition of new lan…
Program slicing provides explanations that illustrate how program outputs were produced from inputs. We build on an approach introduced in prior work by Perera et al., where dynamic slicing was defined for pure higher-order functional programs as a Galois connection between lattices of partial inputs and partial outputs. We extend this approach to imperative functional programs that combine higher-order programming with references and exceptions. We present proofs of correctness and optimality of our approach and a proof-of-concept implementation and experimental evaluation.
Soft constraints extend classical constraints to represent multiple consistency levels, and thus provide a way to express preferences, fuzziness, and uncertainty. While there are many soft constraint solving formalisms, even distributed ones, by now there seems to be no concurrent programming framework where soft constraints can be handled. In this paper we show how the classical concurrent constraint (cc) programming framework can work with soft constraints, and we also propose an extension of cc languages which can use soft constraints to prune and direct the search for a solution. We believ…
Diverse selection statements -- if-then-else, switch and try-catch -- are commonly used in modern programming languages. To make things simple, we propose a unifying statement for selection. This statement is of the form seqor(G_1,...,G_n) where each $G_i$ is a statement. It has a a simple semantics: sequentially choose the first successful statement $G_i$ and then proceeds with executing $G_i$. Examples will be provided for this statement.
In 2008, Ben-Amram, Jones and Kristiansen showed that for a simple "core" programming language - an imperative language with bounded loops, and arithmetics limited to addition and multiplication - it was possible to decide precisely whether a program had certain growth-rate properties, namely polynomial (or linear) bounds on computed values, or on the running time. This work emphasized the role of the core language in mitigating the notorious undecidability of program properties, so that one deals with decidable problems. A natural and intriguing problem was whether more elements can be added …
Leveraging spatial sparsity has become a popular approach to accelerate 3D computer graphics applications. Spatially sparse data structures and efficient sparse kernels (such as parallel stencil operations on active voxels), are key to achieve high performance. Existing work focuses on improving performance within a single sparse computational kernel. We show that a system that looks beyond a single kernel, plus additional domain-specific sparse data structure analysis, opens up exciting new space for optimizing sparse computations. Specifically, we propose a domain-specific data-flow graph mo…
Programmers frequently maintain implicit data invariants, which are relations between different data structures in a program. Traditionally, such invariants are manually enforced and checked by programmers. This ad-hoc practice is difficult because the programmer must manually account for all the locations and configurations that break an invariant. Moreover, implicit invariants are brittle under code-evolution: when the invariants and data structures change, the programmer must repeat the process of manually repairing all of the code locations where invariants are violated. A much better appr…
A number of high-level languages and libraries have been proposed that offer novel and simple to use abstractions for concurrent, asynchronous, and distributed programming. The execution models that realise them, however, often change over time---whether to improve performance, or to extend them to new language features---potentially affecting behavioural and safety properties of existing programs. This is exemplified by SCOOP, a message-passing approach to concurrent object-oriented programming that has seen multiple changes proposed and implemented, with demonstrable consequences for an idio…
Interdisciplinary Centre for Security, Reliability and Trust (SnT)（安全、可靠性与信任跨学科中心（SnT））；University of Luxembourg（卢森堡大学）
The number of cores on graphical computing units (GPUs) is reaching thousands nowadays, whereas the clock speed of processors stagnates. Unfortunately, constraint programming solvers do not take advantage yet of GPU parallelism. One reason is that constraint solvers were primarily designed within the mental frame of sequential computation. To solve this issue, we take a step back and contribute to a simple, intrinsically parallel, lock-free and formally correct programming language based on concurrent constraint programming. We then re-examine parallel constraint solving on GPUs within this fo…
