POCS.Common.NbdAPI

POCS.Common.NbdImpl

POCS.Common.NbdServer

POCS.Common.OneDiskAPI

POCS.Helpers.Disk

• Disk model.
• Model of bytes.
• Model of blocks.
• Disk as a list of blocks.
  • Theorems about diskGet
  • Theorems about diskUpd
  • Theorems about diskShrink
  • Theorems about diskUpds
  • Theorems about diskGets

POCS.Helpers.Helpers

• Decidable equality.
• maybe_holds predicate.
• maybe_eq predicate for equality.
• maybe_eq_list for equality of lists.
• Proof automation.
  • Simplify matches when possible
  • Find and destruct matches
  • Variants of intuition that do not split the goal.
• Instantiate existentials (deex)
  • Other proof automation helpers

POCS.Lab0.Exercises

• Part A: incrementing and swapping.
• Swapping.
• Part B: recursive procedures.
• Recursive procedures on your own.

POCS.Lab0.ThreeVariablesAPI

• Specification of variables.
• Operations on variables.
• Variables module

POCS.Lab1.StatDbAPI

• Specification for StatDB
  • The state of StatDB
  • The initial value of the spec state:
  • The specification of the StatDB operations
• StatDB module

POCS.Lab1.StatDbCli

POCS.Lab1.StatDbImpl

• An implementation of StatDB
  • Exercise : complete the implementation of mean
  • Exercise : complete the implementation of the abstraction function:
  • Exercise : complete the proof for the following admitted examples
  • Exercise : complete the proof of add
  • Exercise : complete the proof of mean

POCS.Lab1.VariablesAPI

• Specification of Variables.
• Variables module

POCS.Lab1.VariablesImpl

• An implementation of Variables.

POCS.Lab2.BadBlockAPI

POCS.Lab2.BadBlockImpl

POCS.Lab2.RemappedDiskImpl

POCS.Lab2.RemappedServer

POCS.Lab3.LogAPI

• Logging API

POCS.Lab3.LogImpl

• Implementation of the atomic append-only log.

POCS.Lab4.ReplicatedDiskImpl

• Helper theorems and tactics for proofs.
• Specifications and proofs about our implementation of the replicated disk API,
• without considering our recovery.
• These intermediate specifications separate reasoning about the
• implementations from recovery behavior.
• Recovery implementation.
• We provide the general structure for recovery: essentially, it consists of
• a loop around fixup that terminates after either fixing an out-of-sync
• disk block or when a disk has failed.
• Theorems and recovery proofs.

POCS.Lab4.ReplicatedServer

POCS.Lab4.TwoDiskAPI

POCS.Lab4.TwoDiskBaseAPI

POCS.Lab4.TwoDiskBaseImpl

POCS.Lab4.TwoDiskImpl

POCS.POCS

• 6.826 lab assignments infrastructure

POCS.Spec.Abstraction

• Specification style: Abstractions with pre- and post-conditions
  • Abstraction relation and composition
  • Specification
  • Correctness of a procedure
  • Proving correctness
  • Reasoning about the Ret return operation.
  • Proof automation
  • step_proc
  • Initialization
  • Initialization specs

POCS.Spec.Proc

• Model of sequential procedures with mutable state.
• Execution model.
• Execution model with recovery
• Chaining normal execution with recovery
• Notation for composing procedures.

POCS.Spec.ProcTheorems

• Automation for inverting execution behavior.

POCS.Spec.Recovery

• Reasoning about crashes and recovery