Improve SymbExLogger#622
Conversation
- Thread safe as long as silicon parallelizes up to the entity level: SymbLog itself is not thread safe. --ideModeAdvanced accordingly does not require --numberOfParallelVerifiers 1 anymore. - Change SymbLog to accept a listener for appropriate events.
|
Regarding thread safety: Generally a good idea, but it seems a bit dangerous to make one logging/reporting component thread-safe, while many others still are not. I don't have a strong opinion here, though, and since you already did the work ... :-) |
|
Is this work in progress or should it be reviewed? In the former case, please convert to a draft (I've actually never used that GitHub feature, but since it exists ...). |
|
This is ready for review! Sorry, did not know if I should re-ping you. |
|
Re-pinging is always a good idea :-) I'll do a review after my holiday, i.e. mid/end August. |
|
@niomaster Please remove the merge conflicts first. Also: why is a ``validateOpt(...) |
|
I resolved the merge conflicts, and the |
mschwerhoff
left a comment
mschwerhoff
left a comment
There was a problem hiding this comment.
Looks good to me.
@ArquintL If you see a reason not to merge, please let me know. Otherwise, I'll merge at the end of the week.
ArquintL
left a comment
ArquintL
left a comment
There was a problem hiding this comment.
I only have a minor comment but otherwise looks good to me too
|
Just in case: I'm working on making the logger externally parallelizable (as is silicon now) as promised in #660 (comment), so please don't merge this right now. |
The root symbexlog comes from Silicon and is computed explicitly on configuration, so it can be overridden From there, the MainVerifier owns the root log, and WorkerVerifiers ask the MainVerifier for a member-scoped symbexlog
- do not use newEntityLogger directly, because it's not inserted in the members of the root log - synchronize on the log instead of the map, because I'm using a var instead of mutable.Map - delay opening the member scope to avoid using early initializers
…n crashing) disallow use of ideModeAdvanced in the presence of parallelizeBranches
pieter-bos
requested review from
ArquintL and
mschwerhoff
and removed request for
mschwerhoff
mschwerhoff
left a comment
mschwerhoff
left a comment
There was a problem hiding this comment.
Looks generally good, modulo the comments I left.
|
@niomaster FYI: We just started preparing the Januar release of Viper, and would be happy to include your changes. |
This reverts commit 505c61b.
|
I've addressed all the comments! |
|
@marcoeilers Linard and I reviewed the PR. Any objections from your side to merge it in now? |
|
No objections, looks good to me. |
|
@niomaster Thanks a lot for your contribution to Viper, Pieter! |
4 participants
A first attempt at some changes to symbexlogger I'd like to see:
SymbLogdoesn't write records into memory directly, but rather does so via aSymbLogListener, so VerCors can listen to the events directly instead of polling the log. Additionaly I don't think we need the history of all records.SymbLogthread safe up to parallelization of entities, as far as I understand that's the current state of silicon (?). If this can be left in I'd be inclined to turn on logging by default if the performance penalty is not too great.Of course happy to address any comments :)