CS 528/428, Spring 2020. Resources

CS 528/428 Resources, Spring 2020

Last modified: January 10, 2011.

This page is still under major construction!

Content

Machine Platform and Hardware Model

  • MIPS simulator
       The MIPS intruction set
  • DLX
  • Turing Machine
  • MIX
       Knuth's page about MMIX

    • Proof Assistants

  • The Coq project.
  • Isabelle/HOL
  • PVS
  • Agda
  • ACL2

    • Operating Systems

  • Nachos
  • OS161
       John Corwin installed OS/161 and its tools on daffy in his home directory. The simulator binaries and tools are in /home/jjc72/cs161/bin. The operating system source is in /home/jjc72/cs161/os161-1.10. All of the OS and simulator archives are in /home/jjc72/os161-arch.
       Here is an overview of the system.
       The OS/161 thread code is in kern/thread/scheduler.c and kern/thread/thread.c. The machine-dependent context switching code is in kern/arch/mips/mips/pcb.c and kern/arch/mips/mips/switch.S.
       A general overview of the code is here. There's also a small manual for system/161 at: http://www.courses.fas.harvard.edu/~cs161/handouts/sys161/.
       Also you can take a look at the first two assignments of cs422. The first is on synchronization and concurrency, and the second is on processes and system calls.
    http://zoo.cs.yale.edu/classes/cs422/assignments/as1.html
    http://zoo.cs.yale.edu/classes/cs422/assignments/as2.html

  • TinyOS
  • SOS
  • MicroC/OS-II
  • Sample Thread Library Code
       The mini thread library written by Zhaozhong.
       Valery's Ultralightweight Scheduler.

    • Verification Tools

  • various verification methods and projects.
    • Copyright (c) 2009-2020, Zhong Shao, Dept. of Computer Science, Yale University.