MIT PDOS

Repositories

• perennial

  Verifying concurrent crash-safe systems

  coq concurrency verification
  Coq MIT 14 58 5 0 Updated Apr 12, 2021

• ward
  C++ 3 23 30 2 Updated Apr 12, 2021

• xv6-public

  xv6 OS
  C 2,467 4,484 1 23 Updated Apr 11, 2021

• goose-nfsd

  Goose NFS server
  Go MIT 0 10 0 0 Updated Apr 10, 2021

• dafny-nfsd

  Combining Perennial and Dafny with a verified journal

  verification dafny
  Dafny MIT 2 4 0 0 Updated Apr 9, 2021

• xv6-riscv

  Xv6 for RISC-V
  C 331 1,161 12 25 Updated Apr 7, 2021

• mcqc

  A Gallina compiler with C++17 as an intermediate representation
  Haskell MIT 6 23 7 (2 issues need help) 0 Updated Apr 5, 2021

• noria

  Fast web applications through dynamic, partially-stateful dataflow
  Rust 155 3,315 42 (7 issues need help) 5 Updated Feb 25, 2021

• zero

  PDOS keybase bot
  JavaScript 0 6 0 0 Updated Jan 2, 2021

• xv6-riscv-fall19

  6.S081/6.828 lab repo for fall 2019
  C 306 133 2 6 Updated Dec 3, 2020

• xv6-riscv-book

  Text describing xv6 on RISC-V
  TeX 37 180 3 2 Updated Nov 29, 2020

• noria-mysql

  MySQL/MariaDB protocol shim for Noria
  Rust MIT 10 55 4 1 Updated Oct 29, 2020

• 6.826-2020-labs

  Lab assignments for 6.826
  Coq 4 5 0 0 Updated Oct 20, 2020

• argosy

  Proving crash safety for systems with layered recovery

  coq verification recovery
  Coq MIT 3 9 0 0 Updated Oct 15, 2020

• perennial-examples

  Examples verified using Perennial
  Go MIT 0 2 0 0 Updated Sep 12, 2020

• new-students

  Welcome for new PDOS students to get access to the organization
  0 0 0 0 Updated Aug 12, 2020

• xv6-book

  Commentary for xv6-public
  Perl 53 176 7 14 Updated Aug 10, 2020

• mailbot

  Bot to send email notifications when pushing to GitHub
  Shell 4 6 0 0 Updated May 18, 2020

• secfs-skeleton

  Skeleton code for new 6.858 final project --- an encrypted and authenticated file system
  Python MIT 1 9 0 0 Updated Apr 14, 2020

• cspec

  Verifying concurrent code with layers and movers
  Coq 1 9 0 0 Updated Feb 18, 2020

• RVirt

  RISC-V hypervisor written in Rust
  Rust Apache-2.0 15 184 0 0 Updated Dec 19, 2019

• 6.828-qemu

  qemu patched for debugging, used for 6.828
  C 33 47 1 1 Updated Nov 29, 2019

• 6.826-2019-labs

  Lab assignments for 6.826
  Coq 2 9 0 0 Updated Nov 8, 2019

• biscuit

  Biscuit research OS
  Go 127 1,835 2 1 Updated Sep 20, 2019

• fscq

  FSCQ is a certified file system written and proven in Coq
  Coq 20 208 4 0 Updated Aug 29, 2019

• noria-ui

  Web UI for Noria clusters
  JavaScript MIT 10 52 0 0 Updated Jul 22, 2019

• perflock

  RWMutex for sharing of multicore machines.
  C MIT 1 15 0 0 Updated May 24, 2019

• noria-benchmarks

  Experiment scripts and results for Soup
  Rust 2 3 5 (2 issues need help) 0 Updated Oct 3, 2018

• soup-dbtoaster

  Soup benchmarks using DBToaster
  Shell 0 0 0 0 Updated Sep 19, 2018

• dsrg Archived

  Distributed Systems Reading Group
  CSS 1 19 0 0 Updated Nov 29, 2017