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

Séance de cours

Concurrence et mémoire transactionnelle en Dafny

Description

Cette séance de cours couvre les bases de Dafny, la concurrence de modélisation, et la mise en œuvre de la mémoire transactionnelle. Il comprend des preuves de sécurité et de vivacité pour la mémoire transactionnelle avancée et basée sur le verrouillage. L'exposé traite également des difficultés et des limites de Dafny, ainsi que des étapes futures dans la réécriture du code en inox, la définition des planificateurs, et la preuve de la sécurité et des propriétés de la vie.

Cette vidéo est disponible exclusivement sur Mediaspace pour un public restreint. Veuillez vous connecter à Mediaspace pour y accéder si vous disposez des autorisations nécessaires.

Regarder sur Mediaspace

Source officielle

Concepts associés (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.

Programmation concurrente

La programmation concurrente est un paradigme de programmation tenant compte, dans un programme, de l'existence de plusieurs piles sémantiques qui peuvent être appelées threads, processus ou tâches. Elles sont matérialisées en machine par une pile d'exécution et un ensemble de données privées. La concurrence est indispensable lorsque l'on souhaite écrire des programmes interagissant avec le monde réel (qui est concurrent) ou tirant parti de multiples unités centrales (couplées, comme dans un système multiprocesseurs, ou distribuées, éventuellement en grille ou en grappe).

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 (abrégé en MCC ou MVCC) est une méthode informatique de contrôle des accès concurrents fréquemment utilisée dans les systèmes de gestion de base de données et les langages de programmation concernant la gestion des caches en mémoire. Le principe de MVCC repose sur un verrouillage dit optimiste contrairement au verrouillage pessimiste qui consiste à bloquer préalablement les objets à des garanties de bonne fin. L'inconvénient logique est qu'une mise à jour peut être annulée du fait d'un "blocage" en fin de traitement.

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.

Afficher plus

Séances de cours associées (32)

Sémantique et vérification des devises

Explore la sémantique, les fonctions récursives, les boucles, la modélisation entrelacée et la vérification de l'interprète.

Vérification formelle et synthèse des programmes

Par l’instructeur Viktor Kuncak explore les activités de vérification formelle, de synthèse de programme et d’enseignement à l’EPFL.

Introduction à la contractualité

Couvre les bases de la concurrence, de son importance et de la façon d'écrire des programmes concomitants.

Programmation asynchrone : rappels et échecs

Couvre le concept de programmation asynchrone et comment gérer les dépendances et les échecs.

Problème de Philosophes de la salle à manger

Discute d'algorithmes pour prévenir la famine et maximiser les philosophes qui mangent simultanément.

Afficher plus

Concepts associés (12)

Concurrency control

Programmation concurrente

Optimistic concurrency control

Multiversion Concurrency Control

Transactional memory

Afficher plus