Language-server-protocol: Protocol consistency gurantees are subtly incorrect

[matklad]

Hi!

This is a rather handwavy and philosophical issue, but I've decided to log it just in case.

One of the requirements for the LSP is to synchronize world view between the client and the server, such that server's positions and ranges actually make sense for the client. LSP places two requirements on the server, to maintain consistency, which I believe are both unnecessary and insufficient for consistency.

The first requirement is to send and maintain document versions together with edits.

The second requirement is about response ordering:

However, the server may decide to use a parallel execution strategy and may wish to return responses in a different order than the requests were received. The server may do so as long as this reordering doesn’t affect the correctness of the responses. For example, reordering the result of textDocument/completion and textDocument/signatureHelp is allowed, as these each of these requests usually won’t affect the output of the other. On the other hand, the server most likely should not reorder textDocument/definition and textDocument/rename requests, since the executing the latter may affect the result of the former.

Let's look closer at the first one, using VersionedTextDocumentIdentifier in edits. The problem with this is that validity of an edit depends not only on the set of files changed, but on the global state of the world. Consider this sequence of events

• client sends a rename request to the server
• server begins handing of the request
• a file C is modified in the client
• server responds to rename requests with modifications to files A and B (declaration and a sole usage, at the time of the request)
• client sends content change notification

Here, the edit from the server might be incorrect, if the change of the C file introduced a new usage, but client can't figure that out using only A and B versions!

Another, more obvious problem with VersionedTextDocumentIdentifier is that it only applies to edits, while results of readonly queries like definition or worksapceSymbols might also get invalidated by changes.

Let's look at the second requirement now. It says that the server is responsible for making sure that its responses are valid for the current state of the world on the client. I would say that it simply is impossible for the server to maintain this guarantee, because ultimately it is the client who owns all of the documents. For example, if client receives a response to the definition request, it might be stale just because user has typed in some text. From the client's POV, edits from the server and from the user are more or less equivalent, and it should be able to deal with both anyway.

So, these two requirements place restrictions on the server (tracking file versions is particularly troublesome), while not providing actual guarantees.

I believe a model which is both simpler and more correct exists. Here's what the Dart server says about the issue:

There is no guarantee concerning the order in which responses will be returned, but there is a guarantee that the server will process requests in the order in which they are sent as long as the transport mechanism also makes this guarantee.

This is strictly more powerful than sending document versions: a client may maintain a global revision counter and use the value of the counter at the time of last modification as a document's version. Then, for each request to the server, it may remember the value of the global revision counter at the time of request. When the client gets back a response, it can check current versions of affected documents against the historical revision, and act accordingly: apply edits if there are no conflicting changes, notify the user about potential conflicts, re-send the query, modify edits themselves to take changes into account. This naturally works for read-only queries like symbols as well.

FWIW, Dart protocol also has file version field, but it is deprecated :-)

So, my suggestion for LSP would be to adopt "client requests and notifications are processed in order" approach to maintaining consistency, make document versions optional (b/c they are a pain to maintain on the server and not exactly useful) and remove any requirements for ordering of server's responses.

[DanTup]

So, my suggestion for LSP would be to adopt "client requests and notifications are processed in order" approach to maintaining consistency, make document versions optional (b/c they are a pain to maintain on the server and not exactly useful)

I don't think this change would provide the necessary guarantees you're hoping for. Even if a server processes all messages to completion in-order, it can't synchronously block the user from typing in the editor, so the server could always still generate edits that were valid at the time they were generated but are now invalid (and overwrite the users recent changes).

For example:

• User opens a file
• User formats document (sends a format request to the server)
• User types some code (sends a didChange notification to the server)
• Server responds to the format request with a full formatted file
• Server processes didChange and updates its internal state with the users changes
• Editor overwrites the users changed code with the formatted version of the original file (which sends another didChange notification to the server)
• Server updates its internal state with the value from client, which is the formatted original document - losing the edits they made

In this case, the server and client both end up in sync, but the users changes were lost. The version identifier for LSP prevents this, because the editor can discard the edit if it knows that it is not based on the same version of the document.

That said - as far as I can tell, formatting doesn't support using the versioned identifiers, so still has the flaw above (I'll open an issue about it). See below comment..

[DanTup]

Actually, I don't think things that are request/response that only modify one file (like formatting) need versioned identifiers - the editor can track this itself - it knows the doc version when it sent a format request and therefore knows whether it's still valid when the response comes through.

[matklad]

so the server could always still generate edits that were valid at the time they were generated but are now invalid

This is precisely the problem: server can always generate invalid edits. The question is, how does the client decide if the edit is safe to apply? The reliable solution to this problem is to track validity of edit on the client side: an edit is valid if there were no modifications since the request that resulted in the edit.

Version Identifiers seem like they solve the problem while they actually don't: and edit might be invalidated by changes to the resources not affected by the edit itself (example: rename request).

The clause about

The server may do so as long as this reordering doesn’t affect the correctness of the responses.

just does not make sense, precisely because it is impossible for the server to only generate correct edits.

[matklad]

@DanTup I see you work on the Dart support, so could you perhaps ask around about the reason why fileStamp was removed from Dart's protocol SourceFileEdit without replacement? I suspect that this is due to a similar realization that "in order processing / out of order response" is necessary & sufficient for providing the strictest possible consistency guarantees, but I am curios about the real reason.

[DanTup]

The reliable solution to this problem is to track validity of edit on the client side: an edit is valid if there were no modifications since the request that resulted in the edit.

It's possible to make edits from the server without a client-initiated request:

"The workspace/applyEdit request is sent from the server to the client to modify resource on the client side."

But I guess it's the same any edit affecting multiple files - the client wouldn't know which documents version numbers to track. I think having it on the server adds some safety: "you can only apply this edit if your document matches this version that I based the edits upon".

Version Identifiers seem like they solve the problem while they actually don't: and edit might be invalidated by changes to the resources not affected by the edit itself (example: rename request).

I'm not sure I understand the example. It's possible to end up with code that's not correct (eg. if you added a reference to a symbol while it was being renamed), but I don't think that's what it's trying to prevent - it's trying to prevent edits to a document that has changed - thus potentially losing the users work.

The clause about

The server may do so as long as this reordering doesn’t affect the correctness of the responses.

just does not make sense, precisely because it is impossible for the server to only generate correct edits.

I don't think this is saying the server must only generate correct edits, but rather just a reminder that if you (the server) are going to re-order requests or process them concurrently, you're responsible for ensuring that they remain correct (for example, reordering two incremental edits is dangerous, as is processing them concurrently such that the second one loses the the first one).

@DanTup I see you work on the Dart support, so could you perhaps ask around about the reason why fileStamp was removed from Dart's protocol SourceFileEdit without replacement?

I haven't worked a lot on the server - I've mostly been a consumer of it for the Dart/Flutter plugins (though I am investigating adding an LSP interface to the server), but if I remember correctly, it was not working correctly and no clients were using it so it was removed (I looked, but unfortunately can't find the discussion).

I suspect that this is due to a similar realization that "in order processing / out of order response" is necessary & sufficient for providing the strictest possible consistency guarantees, but I am curios about the real reason.

The server actually does do some async processing, but has careful handling to try and avoid some of these issues. For example, if you send a file modification while it's calculating a refactor, it may cancel the refactor (CONTENT_MODIFIED error). This is only possible because it may begin processing the edit request while the refactor was being calculated (though worth noting, this is not bulletproof, because you may send an edit while the server is transmitting the refactor edits back).

[matklad]

It's possible to make edits from the server without a client-initiated request:

That's a very interesting observation! Because changes flow from client to server via notification (which don't have responses), client has now way to check which state server was in when it sent the workspace/applyEdit. And this indeed breaks strong consistency guarantees of my proposal.

It's interesting that in Dart, changes are requests (with responses), so the client is able to check which changes were acknowledged when the server-initiated edit is sent (though, IIRC, Dart protocol does not have server-initiated edits).

It's possible to end up with code that's not correct (eg. if you added a reference to a symbol while it was being renamed), but I don't think that's what it's trying to prevent - it's trying to prevent edits to a document that has changed - thus potentially losing the users work.

Yeah, that's exactly the example I had in mind. Sure, "not loosing user's work" is more important then "producing correct results", but I wish that we had both, which seems like it could be achieved by moving bookkeeping to the client, which also simplifies the protocol itself (b/c you don't need versioned identifiers).

I don't think this is saying the server must only generate correct edits, but rather just a reminder that if you (the server) are going to re-order requests or process them concurrently, you're responsible for ensuring that they remain correct (for example, reordering two incremental edits is dangerous, as is processing them concurrently such that the second one loses the the first one).

Probably. The case I am worried about is this:

• client sends workspace/symbols request
• client sends reformat document request

Ideally on the server side I'd just spawn two background tasks on the threadpool, which send responses back in arbitrary order. The client then would have to check if offsets in workspace/symbols are still valid (which it has to do anyway, because the user can just type some code), and fail gracefully if they are stale (by repeating the request or by adjusting the offsets according to the edits or by just using stale offsets).

However that clause seems to imply that I have to complete symbols request before reformat request, which requires additional bookkeeping on the server side.

The server actually does do some async processing, but has careful handling to try and avoid some of these issues. For example, if you send a file modification while it's calculating a refactor, it may cancel the refactor (CONTENT_MODIFIED error).

Yup, we need support for CONTENT_MODIFIED server error in LSP as well.

though worth noting, this is not bulletproof, because you may send an edit while the server is transmitting the refactor edits back).

I think this is bulletproof, in a sense that a client can reliably tell if the edits it got from server are valid. If client sent an edit, it knows that there were changes since it had initiated the refactor, so it can fail/retry gracefully.

[DanTup]

It's interesting that in Dart, changes are requests (with responses)

Yeah, one thing that LSP is not very clear on IMO is how to handle errors from notifications. For example if a server gets a didChange notification that has line numbers that appear to be out of bounds, what does it do? I'm currently sending showMessage/logMessages but it seems like there should be some guidance around this (of course, it shouldn't happen, but, well, bugs :-))

Yeah, that's exactly the example I had in mind. Sure, "not loosing user's work" is more important then "producing correct results", but I wish that we had both, which seems like it could be achieved by moving bookkeeping to the client

I don't think it's really feasible. Maybe there could be a single version number that changes on any document edit, but it'd probably result in many more dropped edits (unless the client knows which are safe to try with the latest state, but it seems like a minefield). That said, as a user, if I rename a symbol and then write more code that calls the old name while the rename is in progress, I wouldn't really expect it to update my new reference?

The case I am worried about is this:

• client sends workspace/symbols request
• client sends reformat document request

Is this possible? I thought moving focus away from the workspace symbol list would close/cancel the request?

I think this is bulletproof, in a sense that a client can reliably tell if the edits it got from server are valid. If client sent an edit, it knows that there were changes since it had initiated the refactor, so it can fail/retry gracefully.

Right, but wouldn't that require the client to keep track of every document version for every request it sends out (or a single version as noted above)? That seems like quite a burden.

[dbaeumer]

That is a very interesting discussion. The only guarantee the LSP tries to make is that if edits are applied to a document on the client side the version of the document is the same as on the server side when the edits got computed.

Inter file dependencies are not considered in LSP and we can have a discussion how to add this if users think that is necessary. But even if we do (as mentioned above) strict order will not by itself solve this. Something like this always requires deep knowledge of the programming lanuage.

Regarding the format request: the reason why this has no version identifier is that the client initiated the request. If the client could for example block user input while the request is running no additional checking is necessary. If the client allows user input the client needs to track this and ignore the format request result. In VS Code we do the following: all requests that could modify stuff (for example format) are canceled if the document they will be applied to changes in any ways. The LSP client even send the cancel to the server which would allow for canceling the format computation on the server side. I think this is what you meant by doing the book keeping on the client.

[dbaeumer]

I do like the addition of a CONTENT_MODIFIED standard error so that clients uni-formally handle this.

[matklad]

Is this possible? I thought moving focus away from the workspace symbol list would close/cancel the request?

That is indeed a good question. In practice, I expect that this discussion is irrelevant for the actual user experience: given that humans are slow, I expect real race conditions to be extremely rare in practice.

Right, but wouldn't that require the client to keep track of every document version for every request it sends out (or a single version as noted above)? That seems like quite a burden.

I think there's an impl that would work: we can have a single global version that is incremented on every edit, plus a document version, which is equal to global version at the time of last document modification.

That way, if we tag each request with global version as well, we can answer the question "was this particular document modified since this request".

Or, to wrap this around, the client library can have a global counter of server requests, and use a client-side document changed listener, which maintains a map from document to "this document last changed at request X".

I also think that a single global version solution won't suffer too much from "dropped edits" problem, precisely because concurrent edits are rare. If I understand correctly, IntelliJ client for dart cancels all in-flight requests if any modification happens.

No matter how you put, if you want strict correctness guarantees (which you might not want), someone, either client or server, will have to manage versions. The client just happens to have more information to do this.

[DanTup]

Regarding the format request: the reason why this has no version identifier is that the client initiated the request.
...
In VS Code we do the following: all requests that could modify stuff (for example format) are canceled if the document they will be applied to changes in any ways.

I think it may be worth adding a note to the spec about this (assuming it's intended for editor/client authors too) to ensure that other editors/clients implement something to protected against corrupting files if they're modified (it's less obvious when the API doesn't have a version in the response - maybe it's worth them being consistent to simplify things? it's a bit breaking though).

[matklad]

But even if we do (as mentioned above) strict order will not by itself solve this. Something like this always requires deep knowledge of the programming lanuage.

I am not sure I fully agree here. A conservative approximation "if anything changes, assume all edits requests are invalid" seems to be feasible to implement, and could have a good UX (b/c concurrent modifications are rare, and because retrying can be implemented transparently).

But, again, I am not sure it's worth doing this.

[DanTup]

given that humans are slow, I expect real race conditions to be extremely rare in practice.

Yeah, but they all turn up when you're writing integration tests instead (speaking from experience :-))

I think there's an impl that would work: we can have a single global version that is incremented on every edit

Is it valid for servers to generate edits outside of the workspace root? If so, this might fall down (I'm not sure if they are, but it is possible to open "loose" files).

If I understand correctly, IntelliJ client for dart cancels all in-flight requests if any modification happens.

Hmm, that's interesting, I wonder what the consequences of not doing that in the VS Code plugin are. It's possible in most cases VS Code is dropping the response anyway, so it might be equivalent.

[matklad]

If I understand correctly, IntelliJ client for dart cancels all in-flight requests if any modification happens.
For example, if you send a file modification while it's calculating a refactor, it may cancel the refactor (CONTENT_MODIFIED error).

An interesting observation: the experimental language server for Rust I am writing has exactly the same behavior: when a modification arrives on the server, it cancels all in-progress requests.

I suspect a lot of servers can use the same model, because it seems the best among possible choices:

• When edit arrives on the server, one can wait for all pending request to be finished before applying the edit. This seems sub optimal, because old results are probably not needed anymore, and because the speed with which you react to edits is important for overall latency.

• Another choice is to use purely immutable data structures throughout a server, so that applying edit creates new state, while pending requests can finish with old state. This seems sub optimal: immutable data structures use more memory, force you to use a specific programming model and, again, the results of pending requests are probably not interesting any more.

• The third choice is to cancel all pending requests, gain exclusive access to the server's state and apply changes in place.

[DanTup]

Are you concerned about overlapping requests that both modify the state of documents, or a modification overlapping an in-progress request that builds an edit? The first may be a concern if you're multi-threaded (Dart is not, and our applying of edits is synchronous so this can't happen), but I don't think the second is solved by this, since it doesn't eliminate the possibility of sending stale edits (there's always a chance - albeit smaller) that the server is halfway through writing the edit to the output stream as the client is writing a modification event to the input stream.

[matklad]

Not sure I understand the question. My last comment was about overlapping "documentChanged" notification and any request (for example, file outline request).

If you are computing an outline, or highlighting, or just about anything else, you need to make sure that the underlying language server data won't change under your feet, or the server itself might die with some exception.

Again, I don't try to eliminate the possibility of stale edits: on the contrary, I want to embrace the fact that stale results are always possible, and equip the client with a reliable (with one-sided error) way to tell if a particular result is guaranteed to be fresh, or could be stale.

[DanTup]

you need to make sure that the underlying language server data won't change under your feet, or the server itself might die with some exception

Oh, I see. I thought you were concerned about returning incorrect data as a result of the change, rather than something going wrong. I think the solution to that is very server-specific and depends a lot on your implementation, I don't think it could be solved by the protocol?

[matklad]

I don't think it could be solved by the protocol?

Agree. My point was that "modification notification cancels in-flight request" strategy seems like a strategy which a significant fraction of servers would use, and that this strategy is the server-side flavor of "global version counter cancels prior request" client-side behavior. That is, its an argument for "global version counter is not as bad as it seems".

[dbaeumer]

Reading through this again I would propose we do the following things:

• add CONTENT_MODIFIED to the list of error codes
• clarify how clients should handle open request when they support modifying content in parallel (e.g. canceling the request)
• alternatively they can block user input.
• what a server should do if it receives content changes or file change events and is in the process of computing something (e.g. return content modified).

[DanTup]

Sounds reasonable to me - though honestly I don't see how content_modified adds any consistency guarantees. As far as I can see, it only gives the server a documented response to send to a request that it knows is no longer worthwhile (eg. allowing it to short-cut and save some resources).

There's always a chance the server will respond with a (now stale) response even after the client has sent an update, so the client needs to always be ready to handle stale responses (eg. by dropping edits that have version numbers that no longer match the local doc).

[matklad]

I don't see how content_modified adds any consistency guarantees.

Indeed it doesn't, but it doesn't aim to. What ContentModified achieves is that it gives servers a standard error code for "I can't handle quires if you simultaneously mutate the data". That is useful for clients to achieve better UX: instead of showing an error, just retry the request.

[DanTup]

Ok cool, sounds like we're on the same page then (I was just a bit mislead by the title of the issue) 👍

[dbaeumer]

Whats about this:

Language servers usually run in a separate process and client communicate with them in an asynchronous fashion. Additional clients usually allow users to interact with the source code even if request results are pending. We recommend the following implementation pattern to avoid that clients apply outdated response results:

• if a client sends a request to the server and the client state changes in a way that the result will be invalid it should cancel the server request and ignore the result. If necessary it should resend the request to receive an up to date result.
• if a server detects a state change that invalidates the result of a request in execution the server should error these request with ContentModified. Clients can then resend the request if appropriate.

[matklad]

:+1: I'll also add "if client receives a ContentModified error, it generally should not show it in the UI for the end-user". That is, ContentModified is not really an error condition, it's a normal outcome.

[DanTup]

Additional clients usually allow

Should this be "Additionally?"

the server should error these request with ContentModified

I presume should here is as RFC 2119 (eg. recommended, not required)? Some servers may find it difficult to do this if they're single-threaded like Node/Dart. (I ask because this document is full of shoulds that in some cases maybe are requirements? :-))

[dbaeumer]

I made the should a can. IMO the final guard to not apply invalid results is the client. Even if the server doesn't error these requests the client needs to check.

Add the proposal from @matklad about not showing ContentModified in the UI.