Fix analysis auxiliary data marshaling #354
Conversation
| if get_string "load_run" <> "" then ( | ||
| Spec.init (Some (Serialize.unmarshal (Filename.concat (get_string "load_run") "spec_marshal"))) | ||
| ) | ||
| else | ||
| Spec.init None; |
There was a problem hiding this comment.
Spec.init is much earlier than the rest of unmarshaling, not sure if this matters.
There was a problem hiding this comment.
In principle it should not, just be aware that if this marshaled data contains e.g. references they will not point to the same things after marshaling in as references e.g. in the marshaled in hash table, even if they did when it was marshaled out (which has also related to the issue with hashconsing), but hopefully no analysis has such things in its hash table.
There was a problem hiding this comment.
Well, the marshaling for analysis-specific data is very much related to what's in the solution. So this is a very relevant point.
For mallocWrapper hashtable it doesn't matter that the physical objects are not the same, just that both unmarshals separately get objects which have matching identity (by equal/hash).
So following this logic, all marshaled data should be put in a single file using a wrapping record, such that their inter-references are preserved properly. And that no blocks need to be duplicated on disk or after unmarshaling.
| let marshal = Spec.finalize () in | ||
| if get_string "save_run" <> "" then ( | ||
| Serialize.marshal marshal (Filename.concat (get_string "save_run") "spec_marshal") | ||
| ); |
There was a problem hiding this comment.
Spec.finalize is much later than the rest of marshaling, not sure if this matters.
There was a problem hiding this comment.
When marshaling happens here is irrelevant.
There was a problem hiding this comment.
If marshaling is to be done as a single object, like I'm now thinking above, this cannot be separate like this, but everything is unmarshaled/marshaled together. This just means all the solver data etc needs to be kept around for saving this late and all the solver etc data needs to be loaded earlier for init.
|
|
||
| let name () = S.name () ^" hashconsed" | ||
|
|
||
| type marshal = S.marshal (* TODO: should hashcons table be in here to avoid relift altogether? *) |
There was a problem hiding this comment.
Not sure if this would help, this table would be completely disconnected from the marshaled solution, right?
There was a problem hiding this comment.
If spec marshaled data goes together with solution, then it's no longer disconnected. I didn't try this but just thought that maybe if all hashconsing tables are marshaled (not sure if they can though, they use weak data structures internally) and restored, all the solver data is already consistent with hashconsing and nothing needs to be relifted.
It would possibly increase the amount of marshaled data, but also save us from all the trouble of relifting.
There was a problem hiding this comment.
if all hashconsing tables are marshaled (not sure if they can though, they use weak data structures internally)
It does indeed not look like this is possible, as the implementation of BatHashcons.Table uses Weak which cannot be marshaled (see here: https://ocaml.org/api/Weak.html, the documentation is referring to the Marshal module by the standard library, but you also get an error Fatal error: exception Invalid_argument("output_value: abstract value (Abstract)") if your try to marshal the hashcons-tables with Batteries.Marshal.output).
There was a problem hiding this comment.
It should still be possible to temporary convert anything still present in the weak hashtable into a normal one for marshaling purposes. If everything gets added back in the correct order during unmarshaling, it should be equivalent.
That would still involve some extra work on the hashtable, but it might not require calling relift on everything in the solution and needing relift to recurse into inner values through multiple layers. And if it works, then it would also allow removing relift from the interface, which is good for cleanup.
+1 |
3 participants
Closes #352.
TODO
In analyses:
Hashtbls?GoblintUtil.create_vars?RichVarinfos?Since the rest of analyses (besides mallocWrapper) don't seem to have broken under marshaling due to a similar reason, I'm not sure if it's worth the time to go through all analyses to fix such
Hashtbls andcreate_vars. Some OSEK/ARINC stuff uses them extensively.My proposal would be not to for the time being. If an issue appears, it can be fixed because the marshaling interface is now there. If we at some point remove unmaintained analyses, then it's not worth trying to fix and risk introducing new bugs, when they'll get removed anyway.