[cs63201] code verification description submission

[Mikhail Nesterenko]

Mikhail Nesterenko wrote:
> AOS students,
> 
> All who submitted CVDs should by now get my comments. If I asked to
> update and resubmit, please do so by 11:59pm on Friday March 5th.  If
> you have not submitted a CDV at all (and have not made arrangements
> with me), submit by the second deadline. It is two points off the
> projects grade.

Another note. There are two stages to verifying the correctness of the
algorithm:

- "use cases" -- several example computations that can be checked by
  hand that demonstrate the operation of the algorithm

- automated testing - a more extensive (several hundred or thousand of
  states) computations that are verified automatically. Since the
  verification cannot be done by hand, you have to create a
  "verification tool". This tool may be a standalone program or
  a module inside your program, or the part of the simulation engine
  that keeps track of the computation and assures its correct
  behavior.

  For example, for lamport's logical clocks, the tool may keep track
  of the event causality and make sure that the consistency property
  is satisfied. It may be implemented as a part of the simulation
  engine.

  Note that this automated tool has to be verified itself. Possibly 
  through the above use cases.
  
For your project. You have to do both stages of verification.

Thanks,
--
Mikhail