Lamport TLA+ Course Lecture 6: Two-Phase Commit (HD)
Рет қаралды 9,199
Күн бұрынIMPORTANT NOTE!: This is a mirror of Lamport's TLA+ lecture videos with some chapter markers in the video description from Lamport's site for ease of viewing on mobile devices, or other platforms and connection setups where KZfaq is the most optimal "format". For the original files, resources, errata, and more, please visit lamport.azurewebsites.net/vide... or the original page which is linked below.
Original Description: How commitment is achieved, in marriage and database transactions. You also learn about records in TLA+ and some more about using TLC.
Original Link: lamport.azurewebsites.net/vide...
Corrections: lamport.azurewebsites.net/vide...
Contents
0:00 - Intro
00:05 - Prologue
00:32 - Records
01:57 - Weddings
04:30 - The TLA+ Spec
12:14 - The Rest of the Spec
15:42 - Checking the Spec
16:50 - Model Values
19:27 - Correctness of Two-Phase Commit
20:48 - Correctness of Two-Phase Commit
@tlavideocourse8540 5 жыл бұрын
Corrections: lamport.azurewebsites.net/video/corrections.html#lecture6
@twodirectionalfoil 2 жыл бұрын
"stop the video and convince yourself" 😆
@AnonyoX 5 жыл бұрын
Adding TCConsistent as Invariant in TLC shows error "Unknown operator: `TCConsistent`". Is there anything special we need to do other than using "TC == INSTANCE TCommit" in the TwoPhase spec?
@baganatube 5 жыл бұрын
Drop the "TC == ", just "INSTANCE TCommit". Or, type "TC!TCommit" in the invariant box.
@andrewhzy7372 10 ай бұрын
don'e know wahere to find the spec code, when he says copy and past the spec code from the web page, can anyone share with me the web page?
@YoussifSalama 9 ай бұрын
You have to visit the original website it’s uploaded too. It’ll then pop under the video when he mentions it
Scary Teacher 3D Gaming
Рет қаралды 50 МЛН
TESLA CAR WORLD
Рет қаралды 26 М.
Anton Petrov
Рет қаралды 316 М.
TLA+ Video Course
Рет қаралды 3,5 М.
Turing Awardee Clips
Рет қаралды 15 М.
Scary Teacher 3D Gaming
Рет қаралды 50 МЛН