(Downloads - 0)
For more info about our services contact : help@bestpfe.com
Table of contents
1 Résumé
1.1 Introduction
1.1.1 Contexte
1.1.2 Preuve vérifiée par ordinateur de programmes
1.1.3 Parallèlisme
1.1.4 Vérification de programmes parallèles
1.1.5 Plan
1.2 Programmation BSP impérative
1.2.1 Différents types d’opérations BSP
1.2.2 Choix pour BSP-Why
1.2.3 Erreurs fréquentes dans les programmes BSP
1.3 L’outil BSP-Why
1.3.1 Le langage BSP-Why-ML
1.3.2 Transformation des programmes BSP-Why-ML
1.4 Étude de cas
1.4.1 Algorithmes BSP basiques
1.4.2 Construction parallèle d’espaces d’états
1.5 Sémantiques formelles
1.5.1 Sémantiques à grand-pas, et à petit-pas
1.5.2 Sémantiques en Coq
1.5.3 Preuve de la transformation
1.6 Conclusion
1.6.1 Résumé des contributions
1.6.2 Perspectives
2 Introduction
2.1 Context of the Work: Generalities and Background
2.1.1 Why Verify Parallel Programs?
2.1.2 Why is Verification of Parallel Programs Hard?
2.2 Machine-checked Proof of Programs
2.2.1 Common Methods for Having Machine-checked Correct Programs
2.2.2 Hoare Logic and Deductive Verification of Programs
2.3 Parallel Computing
2.3.1 Different Forms of Parallelism
2.3.2 The Bulk-Synchronous Parallelism
2.4 Verification of Parallel Programs
2.4.1 Generalities
2.4.2 Advantages of Bridging Models for Correctness of Parallel Programs
2.4.3 Our Approach: Deductive Verification of BSP Programs
2.5 Outline
3 Imperative BSP Programming
3.1 Different Kinds of BSP Operations
3.1.1 Generalities
3.1.2 Description of these Routines
3.2 Some Details About Some BSP Libraries
3.2.1 The Message Passing Interface (MPI)
3.2.2 BSPLIB Like Libraries for C
3.2.3 BSP Programming over Multi-cores and GPUs
3.2.4 BSP Programming in Java
3.2.5 Other Libraries
3.2.6 Which Routines for BSP-Why
3.3 Common Errors Introduced in BSP Programming
3.3.1 Common Errors and Bugs
3.3.2 These Errors in BSP Programs
3.4 Related Works
3.4.1 Parallel Libraries and Imperative Programming
3.4.2 Other Parallel Paradigms
4 The BSP-Why Tool
4.1 The BSP-Why-ML Intermediate Language
4.1.1 Syntax of BSP-Why
4.1.2 The Parallel Memory Model in Why
4.2 Transformation of BSP-Why-ML Programs: the Inner Working
4.2.1 Generalities
4.2.2 Identification of Sequential Blocks
4.2.3 Block Tree Transformation
4.2.4 Translation of Sequential Blocks
4.2.5 Translation of Logic Assertions
4.2.6 Dealing with Exceptions
4.3 Dealing with Subgroup Synchronisation
4.3.1 Subgroup Definition
4.3.2 Transformation of Programs with the Subgroup Synchronisation
4.4 Related Work
4.4.1 Other Verification Condition Generators
4.4.2 Concurrent (Shared Memory) Programs
4.4.3 Distributed and MPI Programs
4.4.4 Proof of BSP Programs
5 Case Studies
5.1 Simple BSP Algorithms
5.1.1 Parallel Prefix Reductions
5.1.2 Parallel Sorting Algorithm
5.1.3 Mechanical Proof
5.2 Parallel State-space Construction
5.2.1 Motivations and Background
5.2.2 Definitions and Verification of a Sequential State-space Algorithm
5.2.3 Verification of a Generic Distributed State-space Algorithm
5.2.4 Dedicated Algorithms for Security protocols
5.3 Related Work
5.3.1 Other Methods for Proving the Correctness of Model-checkers
5.3.2 Verification of Security Protocols
5.3.3 Distributed State-space Construction
6 Formal Semantics
6.1 Big-steps Semantics
6.1.1 Semantics Rules
6.1.2 Co-inductive Semantics
6.1.3 Adding the Subgroup Synchronisation
6.2 Small-steps Semantics
6.2.1 Semantics Rules
6.2.2 Co-inductive Semantics
6.2.3 Equivalence Between the Semantics
6.2.4 Adding the Subgroup Synchronisation
6.3 Semantics in Coq
6.3.1 Mechanized Semantics in Coq
6.3.2 Memory Model
6.3.3 Environment of Execution
6.3.4 Semantics Rules
6.3.5 Adding the Subgroup Synchronisation
6.4 Proof of the Translation
6.4.1 Program Correctness
6.4.2 Equivalence Between Elements of the Semantics
6.4.3 Elements of Proof in Coq
6.5 Related Work
7 Conclusion
7.1 Summary of the Contributions
7.2 Future Work and Perspectives
7.2.1 Close Future Work
7.2.2 Long Term Perspectives
Bibliography
