coop/preempt [was: Re: release and thoughts]

Billy Tanksley
Wed, 23 Aug 1995 16:00:21 -0700 (PDT)

On Wed, 23 Aug 1995, Patrick Premont wrote:

> > > Implementing coop will be incredibly easy.  Implementing proofs will be 
> > > dramatically harder, BUT will allow many good things.

> > a) (safe coop <=> proofs) /\ (proofs are hard) => (safe coop is hard)
> >    q.e.d.

The first premise here is incorrect.  Safe coop requires proofs, BUT 
proofs do not result ONLY in safe coop.  Proofs result in a universal 
runtime speedup, at the expense of a one-time (constant) speed loss.

> > b) many good things in the far future are worse than some good things now.

> But TUNES is a Usefull Not Expedient System.


Let me add that this can be implemented in parts-- we needn't make our 
multitasking completely safe from the start, just as long as we have the 

> I think this whole debate over coop VS preempt multitasking is being
> done far too early. We should implement preemptive multitasking and
> only once we have the HLL working with a proof system should we
> consider adding transparent cooperative multitasking to increase performance
> when/if it can. But before that we'll be using the proof system to get
> far more important performance increases like proving the type or the
> value of something at compile type (partial evaluation time).

Just as long as we're aware while we write the programs that we will need 
to have a yield in there sometimes, if only to make it easier for the 
proof system.  True, the initial compiler will just compile them out.

> Patrick