Lecture

Concurrency Semantics and Verification

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 covers the semantics and verification of concurrent programs, focusing on recursive functions in relational semantics, loops as a special case, and the need to model interleaving in concurrency. It also discusses difficulties in semantics, verifying an interpreter for a concurrent program, and running an interpreter on a schedule. The lecture concludes with the concept of running an interpreter on a schedule and the challenges of verifying concurrent programs.

Official source

Related concepts (32)

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.

Concurrency (computer science)

In computer science, concurrency is the ability of different parts or units of a program, algorithm, or problem to be executed out-of-order or in partial order, without affecting the outcome. This allows for parallel execution of the concurrent units, which can significantly improve overall speed of the execution in multi-processor and multi-core systems. In more technical terms, concurrency refers to the decomposability of a program, algorithm, or problem into order-independent or partially-ordered components or units of computation.

Semantics

Semantics () is the study of reference, meaning, or truth. The term can be used to refer to subfields of several distinct disciplines, including philosophy, linguistics and computer science. In English, the study of meaning in language has been known by many names that involve the Ancient Greek word σῆμα (sema, "sign, mark, token"). In 1690, a Greek rendering of the term semiotics, the interpretation of signs and symbols, finds an early allusion in John Locke's An Essay Concerning Human Understanding: The third Branch may be called σημειωτική [simeiotikí, "semiotics"], or the Doctrine of Signs, the most usual whereof being words, it is aptly enough termed also λογικὴ, Logick.

Operational semantics

Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms (denotational semantics).

Related lectures (33)

Transaction Management & Concurrency Control

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

Inductive Propositions: Understanding Evaluation in Coq

Covers inductive propositions in Coq, focusing on evaluation rules for arithmetic expressions and their applications in defining partial and non-deterministic functions.

Verifying Programs with Stainless: Part 2

Focuses on using Stainless for program verification, demonstrating the process of verifying programs and ensuring correctness.

Concurrency with Futures

Explores futures as a structured approach to concurrency, simplifying parallel tasks and input-output operations.

Hardware Verification using High-Level Design Languages