IOSerialize and IODeserialize testing wrt. unseen string problem #107
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR aims to address a problem with how TLC deserializes string values that did not come from the same run of TLC.
For now, it consists of a failing test that shows the issue.
IODeserialize allows TLC to ingest arbitrary (supported) TLA+ values using the same mechanism that TLC uses for state checkpoints. This almost always works, except for an interaction with string interning.
All strings TLC "sees" are interned in a table, indices into which are used for efficient string comparisons. On state checkpoint, TLC stores both the table and the string objects. The string objects contain indices into that particular TLC process's string table. That's fine, as long as the values are only loaded by either the same TLC instance, or one that restored the same string table from a checkpoint.
The current version of IODeserialize addresses the problem partially, in that it looks up strings in its string table by value regardless of the serialized table index. This means that two TLCs with the same table entries in a different order are compatible. The problem is that IODeserialize can be used outside of this safe condition as well. We can load value dumps from completely unrelated TLC processes (which could be processing specs containing strings we haven't seen), and we can also generate binary files outside of TLC entirely (my use case, incidentally).
Strings that exist as literals in the TLA+, or were previously generated at any point of the same TLC process's runtime, are safe to load. Loading a previously non-interned string, however, creates a StringValue object with a null
val
pointer, which will crash TLC whenever the value is next accessed. For example, printing it is what I use in the included test.