QUESTIONS & ANSWERS

1. When you wrote "requirements" do you mean the "Notes" you wrote? Apart
from the Notes, there are no requirements mentioned.
No, I mean what should be demanded of the calling programs so that everything works as it should.
2. What are the desired properties of each procedure? do you mean what does
each procedure suppose to do?
I mean what each is supposed to do and how they are supposed to work together and with the calling programs.
Can you put on the web a link to a Questions and Answers table?
okay

> The tasks as specified are a bit unclear to me. Can you please explain what
> exactly is needed to be done? Does expressig the requirements mean to use
> TL, and the propertirs are the invariants ?

TL is one possible language in which to express the requirements and properties.
Invariants are one way of proving many of the properties that the procedures
must have for them to work right.

> Can I submit the exam hand written to your box?

please don't; you can use plaintext

  1. If I understand correctly, use(k,in,out) reads track #k, copies its contents to out, and writes to that track the contents of in. But how can a user just read, or just write?
The procedure use does no reading or writing itself; the driver does.  You need not worry about how the driver knows from the value of the parameter in whether the user wants to read or write or both.
  1. Can I assume (from the comments flaced inside get and finished) that the driver program looks like this:

    2.     local variables: in, out
        do forever {
            get(in)          // in <-- arg
            read(out)        // out <-- track #pos
            write(in)        // track #pos <-- in
            finished(out)    // buf <-- out
        }
    ?
No you cannot assume this, but if you think the driver MUST look exactly like this, then that is part of the requirements for the driver that you may include as part of your answer.

You want the weakest requirements that  guarantee that the scheduler can do its job.

    Btw, this program, implied from get and finished, must do both reading and writing on every cycle, which brings me back to my 1st question.
Same answer.
  1. In question #1, what do you mean by requirements from users and driver? Is it the "P"-part in a {P}S{Q} specification, or both P and Q?
Both P and Q and perhaps more.
    Or do I need to give PTL propositions that must be satisfied by the system?
PTL is one way to specify additional requirements.
1. Shouldn't the parameter of "get" be an out parameter and the parameter of "finished" an in parameter?
in and out are just parameter names.  They are named from the point of view of the disk: in is what is coming in to be written.  We are not concerned that the driver does its job correctly only that the scheduler does.
2. Is the program intended to be incorrect?
Suppose the driver calls Get and assigns -1 to pos. Now if two users call use at the same time, pos may get either one of the positions and both users may use the disk in the time, what should cause a real mess...
The program is still believed to be correct.  Only the driver read/writes.  As stated in the problem, only one (user or driver) process can execute any of the scheduler procedures at any given time.  That is an assumption you are to make of the way the system implements this code.
3. Are there any corrections so far?
No, but see the question and answer file on the course webpage.
What is exact difference between tasks 2 and 3?
Does 3 is a different task or just additional information
to task 2?
3 may mean adding invariants, lemmas, or the like so that the properties you give in 2 are provable.

> What kind of requirements should we find:
> should we be able to prove them from properties in 2 or not?

You will assume that the user and driver requirements are fulfilled when
proving that the desired properties (e.g. no deadlock) hold for the scheduler.

I understand only one process can execute at the same time. Let me rephrase my scenario:
- The driver invokes Get and sets pos to -1. It then waits.
- One user process now calls Use and checks if pos=-1.
- Now the OS (i.e. the system) transfers the control to another user process, which also calls Use and checks if pos=-1.
Okay, I think I didn't make it clear enough that the system does not interrupt any procedure,
unless a process goes to sleep at a wait.  So the first user process will stay in control until
it reaches the wait on stored.
Should we prove:
requirements --> properties
or
properties --> requirements?
The former.
 Should we express semantics of synchronization commands as part of system requirements or can we assume that theorem-prover "knows" about them.
You must express all such matters.
In task no. 2
should we relate to the global variables at all?
or should we just formalize propositions like "no deadlock"?
Only if you need to, but I think you will need to refer
to them for some of the properties you may want.
And if not in the properties, then perhaps in the assumption
that the driver behaves properly.
I understand that we are not required to prove anything, but rather give all
that an automatic prover needs for a proof.  Am I correct?
Exactly
It is not completely clear to me whether a property has to be a property of
the procedures as defined, or alternatively may I require properties
regarding the interaction between the procedures (for instance order of
calling etc...)?
Interaction, too.
Can we add auxilary variables (or labels) to the program?
yes, sure
 
* Can we express the answers for 3 in TL?
Sure
* Regarding 2: we want to verify only properties concerning the flow of control, the synchronization and interaction between the procedures,
not things like the order in which we access the tracks, right?
No, I think you should say something about the level of service (that is, about any bound there may be on the number of requests that can get ahead).