Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

IOSerialize and IODeserialize testing wrt. unseen string problem #107

Draft
wants to merge 1 commit into
base: master
Choose a base branch
from

Conversation

fhackett
Copy link

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Development

Successfully merging this pull request may close these issues.

1 participant