Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Lecture

Concurrency and transactional memory in Dafny

Description

This lecture covers the basics of Dafny, modeling concurrency, and implementing transactional memory. It includes safety and liveness proofs for lock-based and advanced transactional memory. The presentation also discusses the difficulties and limitations of Dafny, as well as future steps in rewriting the code in Stainless, defining schedulers, and proving safety and liveness properties.

This video is available exclusively on Mediaspace for a restricted audience. Please log in to MediaSpace to access it if you have the necessary permissions.

Watch on Mediaspace

Official source

Related concepts (12)

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.

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.

Optimistic concurrency control

Optimistic concurrency control (OCC), also known as optimistic locking, is a concurrency control method applied to transactional systems such as relational database management systems and software transactional memory. OCC assumes that multiple transactions can frequently complete without interfering with each other. While running, transactions use data resources without acquiring locks on those resources. Before committing, each transaction verifies that no other transaction has modified the data it has read.

Multiversion concurrency control

Multiversion concurrency control (MCC or MVCC), is a concurrency control method commonly used by database management systems to provide concurrent access to the database and in programming languages to implement transactional memory. Without concurrency control, if someone is reading from a database at the same time as someone else is writing to it, it is possible that the reader will see a half-written or inconsistent piece of data.

Transactional memory

In computer science and engineering, transactional memory attempts to simplify concurrent programming by allowing a group of load and store instructions to execute in an atomic way. It is a concurrency control mechanism analogous to database transactions for controlling access to shared memory in concurrent computing. Transactional memory systems provide high-level abstraction as an alternative to low-level thread synchronization. This abstraction allows for coordination between concurrent reads and writes of shared data in parallel systems.

Related lectures (32)

Concurrency Semantics and Verification

Explores concurrency semantics, recursive functions, loops, interleaving modeling, and interpreter verification.

Formal Verification and Program Synthesis

By the instructor Viktor Kuncak explores formal verification, program synthesis, and teaching activities at EPFL.

Introduction to Concurrency

Covers the basics of concurrency, its importance, and how to write concurrent programs.

Asynchronous Programming: Callbacks and Failures

Covers the concept of asynchronous programming and how to handle dependencies and failures.

Dining Philosophers Problem