Lecture

Concurrency and transactional memory in Dafny

Graph Chat

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Description

This lecture introduces Dafny, a compiled language designed for formal verification, ensuring correct code execution without runtime errors. It covers modeling concurrency, safety rules, liveness properties, and transactional memory concepts. The instructor presents examples and papers on concurrency and transactional memory, emphasizing formal verification and advanced algorithm creation.

Official source

Related concepts (32)

Linearizability

In concurrent programming, an operation (or set of operations) is linearizable if it consists of an ordered list of invocation and response events, that may be extended by adding response events such that: The extended list can be re-expressed as a sequential history (is serializable). That sequential history is a subset of the original unextended list. Informally, this means that the unmodified list of events is linearizable if and only if its invocations were serializable, but some of the responses of the serial schedule have yet to return.

Concurrency control

In information technology and computer science, especially in the fields of computer programming, operating systems, multiprocessors, and databases, concurrency control ensures that correct results for concurrent operations are generated, while getting those results as quickly as possible. Computer systems, both software and hardware, consist of modules, or components. Each component is designed to operate correctly, i.e., to obey or to meet certain consistency rules.

Compiler

In computing, a compiler is a computer program that translates computer code written in one programming language (the source language) into another language (the target language). The name "compiler" is primarily used for programs that translate source code from a high-level programming language to a low-level programming language (e.g. assembly language, object code, or machine code) to create an executable program. There are many different types of compilers which produce output in different useful forms.

Concurrent computing

Concurrent computing is a form of computing in which several computations are executed concurrently—during overlapping time periods—instead of sequentially—with one completing before the next starts. This is a property of a system—whether a program, computer, or a network—where there is a separate execution point or "thread of control" for each process. A concurrent system is one where a computation can advance without waiting for all other computations to complete. Concurrent computing is a form of modular programming.

Compile time

In computer science, compile time (or compile-time) describes the time window during which a language's statements are converted into 0s and 1s for the computer to understand. The term is used as an adjective to describe concepts related to the context of program compilation, as opposed to concepts related to the context of program execution (runtime). For example, compile-time requirements are programming language requirements that must be met by source code before compilation and compile-time properties are properties of the program that can be reasoned about during compilation.

Related lectures (40)

Correctness of Compilers: Part 1

Explores compiler correctness, examples of verified compilers, formal verification, and the challenges of certifying compilers.

Concurrency and transactional memory in Dafny

Covers Dafny basics, modeling concurrency, and implementing transactional memory with safety and liveness proofs.

Akka Streams: Programming Reactive Systems

Covers Akka Streams basics, stream stages concurrency, materialized values, and more.

Transaction Management & Concurrency Control

Explores transaction management, concurrency control, ACID properties, anomalies, and conflict serializability in database systems.

Transactions and ACID: Overview