David suggested this in an email from 13 May 06:
But I'm wondering what to do with asynchronous edits in the display that take
place while we are waiting for the response to an request.
And on a related issue, how to deal with prover- or broker- generated edits
that might not be requested by the display.
Did you consider this with Ahsan? I wonder how the Eclipse mode solves this.
(Also I suspect you and I may have talked about this or a similar race
condition before).
To be clear the problem is when this happens:
Display Broker
user edits
. -------------------------->
. <editobj>
more edits parse,etc
.
.
. <---------------------------
<dispobjmsg>
The "more edits" in the display may occur inside objects replaced by
the replaceobjs in dispobjmsg, for example. In a bit of testing with the
automatic parsing, I think I noticed this happening once: some text I'd just
written vanished! It's a bit tricky to trigger because the broker responds
quickly and the editobjs are sent after a full second of idle time, so you
need to type at just the right moment. (Even harder to trigger with the
manual reparse).
The simplest thing to do is to prevent "more edits" from occuring by blocking
in the display. That maybe doesn't have a too bad behaviour at the moment
playing with small files, small edits and quick parsers, but it probably isn't
ideal.
Otherwise to be more flexible I think we need to provide resolution either
Display-side or Broker-side:
1. Display replay.
The display keeps history of "more edits" and (optionally) the buffer contents
before they occur, i.e. checkpointing when is sent. When
"replaceobjs" arrives, it retracts the edits (restoring the object
boundaries), commits the replaceobjs and then replays the edits. We expect
the replay to work because the replaceobjs doesn't change the buffer contents,
only object information. The edits might have slightly different behaviour
because of changes in object status, but this should only amount to whether a
region turns underlined/red or not.
2. Broker roll-back.
The broker keeps a history of the object layout and contents before
is processed. After a is sent to the display, it waits for an
acknowledgement in a new message to indicate whether the edit succeeded or
not. If the edit did not succeed, it rolls back the object layout to the
previous state.
<----------------------------------
<dispobjmsg>
----------------------------------->
<editresult accept="true"/>
Now (you guessed it) I think the Broker-based solution is better. First,
because the Broker is going to be better at managing this (it would be a
tricky hack in Emacs) and in general our philosophy is that it's better to
solve things once in the Broker than many times, in each display. And second,
this mechanism seems to extend well to edits which are not requested by the
display (perhaps coming from another display, the broker or the prover). At
the moment if those arrive and conflict with the current display we have no
way to resolve them (and we might not even notice the conflict).
If the replacement is as a result of a request from this display, then the
display can choose to accept the edit or not. If the replacement is a request
from elsewhere, it may conflict with what the user has edited locally (we can
tell this by comparing the regions affected by local edits and replaceobjs).
We can then recover in the display by asking if the user wants to discard his
changes or not --- but the display should report the edit result as accepted,
I think. (The broker must thus send an replaceobjs to the requesting display,
if any, first; wait to see if it is accepted there, and then only after try to
propagate it to other displays if it is accepted).
I'm not looking for fully-fledged transaction handling here, I think it's
reasonable to restrict displays to having at most one editobj request
outstanding. On the other hand, if we have multiple displays making edits,
there can be races between them which must be resolved by the broker. (E.g.
the broker commits to the first edit it receives and which is accepted back
successfully, it then sends with an attribute to indicate that
that the result is an edit from elsewhere and must be accepted.)
What do you think?
Unfortunately it is an incompatible change because of the extra message
(although this is only needed in case the display "owns" the edit/file and
wants the chance to refuse edits). We could either try to get that
implemented in Eclipse quickly, or put in a backwards compatibility hack of
some form.
Perhaps for now we should think about the distributed editing model a bit more
carefully before deciding what to do. In the meantime, there are a couple of
small improvements which I think might help in any case, I'll write about them
in another message.
The rather noncommital answer from Christoph from 15 may 06 is excerpted here for historical authenticitiy:
So, the present situation is that in a situation as you describe, the broker
will discard the edits made after an editobj message has been sent, and before
the dispobjmsg is sent. This is what you observed, and I think this is also how
the Eclipse mode behaves. (It may even lock, not sure.)
[...] My gut feeling is that we have to be careful here not to open
a huge can of complications (locking is simple and might not be that bad), but I
can't pin down anything which is wrong with your suggestion.
Clearly, the issue is far from resolved :-}
--
ChristophLueth - 26 Sep 2006