Recent additions/changes (see personal repo) Marc Nieper-Wißkirchen (11 Nov 2022 17:19 UTC)
Re: Recent additions/changes (see personal repo) Shiro Kawai (14 Nov 2022 19:05 UTC)
Re: Recent additions/changes (see personal repo) Marc Nieper-Wißkirchen (14 Nov 2022 19:11 UTC)
Re: Recent additions/changes (see personal repo) Shiro Kawai (15 Nov 2022 08:31 UTC)
Re: Recent additions/changes (see personal repo) Marc Feeley (17 Nov 2022 13:22 UTC)
Re: Recent additions/changes (see personal repo) Marc Nieper-Wißkirchen (17 Nov 2022 13:51 UTC)
Re: Recent additions/changes (see personal repo) Marc Feeley (17 Nov 2022 14:24 UTC)
Re: Recent additions/changes (see personal repo) Marc Nieper-Wißkirchen (17 Nov 2022 14:44 UTC)
Re: Recent additions/changes (see personal repo) Marc Feeley (17 Nov 2022 15:38 UTC)
Re: Recent additions/changes (see personal repo) Marc Nieper-Wißkirchen (17 Nov 2022 16:26 UTC)
Re: Recent additions/changes (see personal repo) Shiro Kawai (17 Nov 2022 20:12 UTC)
Re: Recent additions/changes (see personal repo) Marc Nieper-Wißkirchen (17 Nov 2022 20:32 UTC)
Re: Recent additions/changes (see personal repo) Shiro Kawai (17 Nov 2022 23:02 UTC)
Re: Recent additions/changes (see personal repo) Shiro Kawai (17 Nov 2022 23:13 UTC)
Re: Recent additions/changes (see personal repo) Marc Feeley (17 Nov 2022 20:43 UTC)

Re: Recent additions/changes (see personal repo) Marc Nieper-Wißkirchen 17 Nov 2022 20:32 UTC

Am Do., 17. Nov. 2022 um 21:12 Uhr schrieb Shiro Kawai <xxxxxx@gmail.com>:
>
> On Thu, Nov 17, 2022 at 6:26 AM Marc Nieper-Wißkirchen <xxxxxx@gmail.com> wrote:
>>
>>
>> The problem is that the interrupting thread and the interrupted thread
>> won't be synchronized.  We can only say that the interrupted thread
>> must eventually observe the interrupt.  But this is probably enough,
>> so we should add something along the following lines:
>>
>> The interrupt must be handled eventually as long as the union of
>> intervals in which the interrupted thread has interrupts enabled is
>> unbounded.  (This is some kind of a rewrite of your "bounded"
>> condition.)
>>
>
> So are you going to change the spec that the interrupt  is 'queued' if the current-interrupt-level > 0, and handled after current-interrupt-level drops to 0?  (I think that's the right thing.)

This should be no change; I always meant the interrupts must be queued.

> Another concern is that how interrupt thunk is scheduled if it occurs during executing another interrupt thunk.  Suppose two interrupt occurs in this chronological order:
>
>   1:  (thread-interrupt! T (lambda () (do-X))
>   2:  (thread-interrupt! T (lambda () (do-Y))
>
> If 2 occurs when T is start executing 1's thunk, but before doing actual work (do-X), does the second thunk is run before (do-X), or it is scheduled after the whole (lambda () (do-X)) thunk?

(do-X) runs in thread T.  So 2. will interrupt it.

If you don't want this, wrap (do-X) in (with-interrupts-disabled ...).

> If it's the former case, we might want to disable interrupts automatically before executing an interrupt thunk, much like a signal is blocked automatically in a signal handler in Unix.  Combined with the queued handler model, the inversion of the order may be an issue; that is, thread Tdisables interrupts, another thread interrupts T with do-X, and after a certain time, T enables interrupts.  Then (lambda () (do-X)) start to run, but suppose another thread inerrupts T right before (do-X) is called.   Even the first interrupt occurs long before the second, (do-Y) is executed first unexpectedly.

The spec does not say that the queued interrupts are handled in the
order they are initiated.

This would smell like an over-specification to me, no?