Martin Quinson [Fri, 18 Feb 2022 23:28:19 +0000 (00:28 +0100)]
Split the Comm observers to their own files
Martin Quinson [Fri, 18 Feb 2022 23:05:13 +0000 (00:05 +0100)]
Split TransitionAny and TransitionRandom to their own files
Martin Quinson [Fri, 18 Feb 2022 22:49:02 +0000 (23:49 +0100)]
Revalidate all SafetyChecker tesh now that the output changed
Martin Quinson [Fri, 18 Feb 2022 22:13:26 +0000 (23:13 +0100)]
Make CommDet a plugin on top of Safety
Martin Quinson [Fri, 18 Feb 2022 20:44:14 +0000 (21:44 +0100)]
Further simplifications in CommDet
Martin Quinson [Fri, 18 Feb 2022 20:23:07 +0000 (21:23 +0100)]
CommDet: detached send should be handled. But how?
Martin Quinson [Fri, 18 Feb 2022 20:10:58 +0000 (21:10 +0100)]
CommDet: Enforce deterministic pattern even during backtrack, to simplify the code
Martin Quinson [Fri, 18 Feb 2022 20:00:46 +0000 (21:00 +0100)]
CommDet: tiny simplification
Martin Quinson [Fri, 18 Feb 2022 19:53:18 +0000 (20:53 +0100)]
Add the MPI tag to the Send/Recv Transitions
Martin Quinson [Fri, 18 Feb 2022 19:21:00 +0000 (20:21 +0100)]
Try to fix the MC build on 32 bits
Martin Quinson [Fri, 18 Feb 2022 18:24:26 +0000 (19:24 +0100)]
Document the fact that MC big bang occured
Martin Quinson [Fri, 18 Feb 2022 18:02:06 +0000 (19:02 +0100)]
MC: no need to read the remote request directly
Martin Quinson [Fri, 18 Feb 2022 15:58:37 +0000 (16:58 +0100)]
CommDet: reimplement on top of transitions. Don't mess with requests anymore
The observer->set_comm() is done during the simcall execution on the
appside, but the transition is serialized before this simcall
execution. I need to fiddle the Checker <-> AppSide protocol, again.
Martin Quinson [Fri, 18 Feb 2022 16:10:54 +0000 (17:10 +0100)]
Have the application execute its transition before returning SIMCALL_EXECUTE_ANSWER
This makes the RPC protocol somewhat more complex, but it's mandatory
to get the updated observer.
This is useful in particular to Isend/Irecv observers that have a
set_comm() field that cannot be set before executing the simcall.
CommDet need that field anyway, so let's change the protocol that way.
Martin Quinson [Fri, 18 Feb 2022 09:11:42 +0000 (10:11 +0100)]
Add getters to the TransitionComm* and TransitionAny*
Martin Quinson [Fri, 18 Feb 2022 07:17:42 +0000 (08:17 +0100)]
sonar fixes
- use uintptr_t instead of void* on the Checker side.
They cannot be dereferenced anyway.
- various small things (const, remove empty statements)
Arnaud Giersch [Fri, 18 Feb 2022 15:05:55 +0000 (16:05 +0100)]
Fix sonar issues in ns3 examples.
Arnaud Giersch [Fri, 18 Feb 2022 13:03:45 +0000 (14:03 +0100)]
Fix sonar issues in ns3 bindings.
Arnaud Giersch [Fri, 18 Feb 2022 10:45:25 +0000 (11:45 +0100)]
Try again to enable ns3 for coverage and sonar [ci-skip].
Arnaud Giersch [Fri, 18 Feb 2022 10:30:10 +0000 (11:30 +0100)]
[experimental] Replace long list of excluded libs with a much shorter whitelist.
For now, exclude any lib which is not libsimgrid.
Arnaud Giersch [Fri, 18 Feb 2022 09:32:14 +0000 (10:32 +0100)]
Deprecate sg_host_dump.
It's unused since the removal of the simdag examples.
Arnaud Giersch [Fri, 18 Feb 2022 09:25:24 +0000 (10:25 +0100)]
Fix xbt_log_appender when there is no percent in template.
Martin Quinson [Fri, 18 Feb 2022 00:25:50 +0000 (01:25 +0100)]
Give the comm to {Send,Recv}Transition, as CommDet needs it
Martin Quinson [Thu, 17 Feb 2022 23:22:32 +0000 (00:22 +0100)]
CommDet: preparatory cosmetics
inline a few functions and move some small things around.
Martin Quinson [Thu, 17 Feb 2022 23:06:33 +0000 (00:06 +0100)]
CommDet: inline a function (+cosmetics)
Arnaud Giersch [Thu, 17 Feb 2022 15:02:16 +0000 (16:02 +0100)]
Pylint docs/source/tuto_s4u/*.py.
Arnaud Giersch [Thu, 17 Feb 2022 14:54:36 +0000 (15:54 +0100)]
Pylint teshsuite/*.py.
Arnaud Giersch [Thu, 17 Feb 2022 14:40:05 +0000 (15:40 +0100)]
Pylint examples/*.py.
Arnaud Giersch [Thu, 17 Feb 2022 13:31:38 +0000 (14:31 +0100)]
Pylint docs/find-missing.py, src/simix/simcalls.py.
Arnaud Giersch [Wed, 16 Feb 2022 22:44:39 +0000 (23:44 +0100)]
Pylint tesh.py.
Martin Quinson [Thu, 17 Feb 2022 09:56:42 +0000 (10:56 +0100)]
mist. (fix gcc MC builds)
Martin Quinson [Wed, 16 Feb 2022 21:38:52 +0000 (22:38 +0100)]
Further isolate CommDet in its own file
Martin Quinson [Tue, 15 Feb 2022 08:42:55 +0000 (09:42 +0100)]
CommDet shall become an extension of the SafetyChecker
Martin Quinson [Tue, 15 Feb 2022 08:04:50 +0000 (09:04 +0100)]
make mc::State extendable so that CommDet does not polute it in any case
Arnaud Giersch [Wed, 16 Feb 2022 21:23:55 +0000 (22:23 +0100)]
Use type 'bool' for boolean variables.
Arnaud Giersch [Wed, 16 Feb 2022 18:20:54 +0000 (19:20 +0100)]
Add basic check for failures in deserialization.
Arnaud Giersch [Wed, 16 Feb 2022 15:25:23 +0000 (16:25 +0100)]
Use bounds checking method array::at().
Arnaud Giersch [Wed, 16 Feb 2022 15:16:26 +0000 (16:16 +0100)]
Blank lines (codefactor.io).
Arnaud Giersch [Wed, 16 Feb 2022 14:26:57 +0000 (15:26 +0100)]
Use C++ std::array (sonar).
Arnaud Giersch [Wed, 16 Feb 2022 13:51:44 +0000 (14:51 +0100)]
One less implicit conversion (sonar).
Arnaud Giersch [Wed, 16 Feb 2022 11:25:00 +0000 (12:25 +0100)]
Don't mix public and private data members (sonar).
Arnaud Giersch [Tue, 15 Feb 2022 20:06:00 +0000 (21:06 +0100)]
We want to serialize the pointer, not the pointee!
Arnaud Giersch [Tue, 15 Feb 2022 12:48:17 +0000 (13:48 +0100)]
Ignore local variables without type in snapshot.
Makes test 's4u-mc-bugged1-liveness' succeed when built with gcc.
Use '--log=mc_snapshot.thres:verbose' to activate the debug message.
AFAICS, the affected variable is parameter 'code' in simcall_blocking.
Note that I would have preferred to correct the DWARF loading code, but
I couldn't figure out what was missing.
Arnaud Giersch [Tue, 15 Feb 2022 10:50:25 +0000 (11:50 +0100)]
Kill duplicate function + typos.
Martin Quinson [Mon, 14 Feb 2022 19:15:35 +0000 (20:15 +0100)]
Reduce code dupplication to please sonar
Arnaud Giersch [Mon, 14 Feb 2022 09:12:24 +0000 (10:12 +0100)]
Make logger mc_compare a subcategory of mc.
Arnaud Giersch [Mon, 14 Feb 2022 08:48:20 +0000 (09:48 +0100)]
Revalidate random-bug-nocrash.tesh.
Martin Quinson [Sun, 13 Feb 2022 22:36:20 +0000 (23:36 +0100)]
Revalidate the tesh output of that test whose reduction is now less efficient for some reason
Martin Quinson [Sun, 13 Feb 2022 21:19:46 +0000 (22:19 +0100)]
Implement WaitAnyTransition
Martin Quinson [Sun, 13 Feb 2022 11:39:14 +0000 (12:39 +0100)]
better name
Martin Quinson [Sun, 13 Feb 2022 11:15:01 +0000 (12:15 +0100)]
Sonar fixes
- Pass the constructor parameters to the ancestor (!)
- Make some stuff const
- don't overuse initializer list of constructors for stuff that can be
initialized in the class
- Kill dead code
- 'auto' instead of redundent type
- true/false instead of 1/0
- Also inline a useless function
Martin Quinson [Sun, 13 Feb 2022 10:24:24 +0000 (11:24 +0100)]
Fix MC builds with gcc12 (and make the serialization more robust)
Martin Quinson [Sat, 12 Feb 2022 22:29:21 +0000 (23:29 +0100)]
Implement TestAnyTransition
Martin Quinson [Sat, 12 Feb 2022 18:10:43 +0000 (19:10 +0100)]
Simplify the serialization protocol to implement TestAny & WaitAny in a moment
Martin Quinson [Sat, 12 Feb 2022 15:36:42 +0000 (16:36 +0100)]
implement CommTestTransition
Martin Quinson [Sat, 12 Feb 2022 13:05:50 +0000 (14:05 +0100)]
Fix MC gcc builds :(
Augustin Degomme [Sat, 12 Feb 2022 12:20:59 +0000 (13:20 +0100)]
fix build
Martin Quinson [Sat, 12 Feb 2022 11:30:10 +0000 (12:30 +0100)]
Move dot_label() from Observer to Transition (+ some reorgs)
Martin Quinson [Sat, 12 Feb 2022 10:33:33 +0000 (11:33 +0100)]
SimcallObservers don't need to be cloned anymore
Martin Quinson [Sat, 12 Feb 2022 10:17:46 +0000 (11:17 +0100)]
Improve the final stats reported by SafetyChecker, and revalidate tesh files
Martin Quinson [Sat, 12 Feb 2022 09:46:45 +0000 (10:46 +0100)]
Fix more sonar things
Martin Quinson [Sat, 12 Feb 2022 09:36:00 +0000 (10:36 +0100)]
Better fix for the security warning from sonar: hide the char* buffer
Martin Quinson [Sat, 12 Feb 2022 08:41:39 +0000 (09:41 +0100)]
Fix the security hotspots of sonar
Martin Quinson [Fri, 11 Feb 2022 23:43:22 +0000 (00:43 +0100)]
Revalidate the tesh of some working MC tests
Martin Quinson [Fri, 11 Feb 2022 23:35:23 +0000 (00:35 +0100)]
Revalidate the tesh of the mc-bugged1 test, which output changed but is working
Martin Quinson [Fri, 11 Feb 2022 23:26:41 +0000 (00:26 +0100)]
Fix the depends of iSend/iRecv vs. WaitComm to fix the bugged2 example
Martin Quinson [Fri, 11 Feb 2022 23:13:47 +0000 (00:13 +0100)]
CommWaitTransition mailbox is now valid
Martin Quinson [Fri, 11 Feb 2022 22:21:08 +0000 (23:21 +0100)]
Implement the RandomTransition
Martin Quinson [Fri, 11 Feb 2022 21:28:42 +0000 (22:28 +0100)]
Remove the hostnames from the CommDet patterns: MC does not have this info anymore
Martin Quinson [Fri, 11 Feb 2022 21:20:57 +0000 (22:20 +0100)]
MC: one simplification step
Martin Quinson [Fri, 11 Feb 2022 21:13:16 +0000 (22:13 +0100)]
Make sure that the last stack element is set when an assertion failure occures
Martin Quinson [Fri, 11 Feb 2022 21:06:09 +0000 (22:06 +0100)]
No need to save the observers on the App side now that they are serialized over
Martin Quinson [Fri, 11 Feb 2022 20:47:52 +0000 (21:47 +0100)]
Inline another stupid function
Martin Quinson [Fri, 11 Feb 2022 20:42:46 +0000 (21:42 +0100)]
Objectification of mc::RecordTrace
Martin Quinson [Fri, 11 Feb 2022 20:13:06 +0000 (21:13 +0100)]
Stop copying transitions around since that would shorten the virtual methods
Martin Quinson [Fri, 11 Feb 2022 19:47:03 +0000 (20:47 +0100)]
Inline another useless function in MC and a define symbol
Martin Quinson [Fri, 11 Feb 2022 18:27:29 +0000 (19:27 +0100)]
Start moving classes into the mc/api directory
Martin Quinson [Fri, 11 Feb 2022 18:04:48 +0000 (19:04 +0100)]
Inline a function of mc::api
Martin Quinson [Fri, 11 Feb 2022 17:01:25 +0000 (18:01 +0100)]
fix MC despite clang-format sorting the headers alphabetically while I would prefer not to
Martin Quinson [Fri, 11 Feb 2022 15:54:52 +0000 (16:54 +0100)]
Fix builds with/without MC and with/without clang (hopefully)
Martin Quinson [Fri, 11 Feb 2022 10:28:26 +0000 (11:28 +0100)]
Prepare to debug the depends
Martin Quinson [Fri, 11 Feb 2022 10:21:20 +0000 (11:21 +0100)]
MC does not need the exact value of the timeout, only where a timeout was specified
Martin Quinson [Fri, 11 Feb 2022 10:16:29 +0000 (11:16 +0100)]
don't use char* for pointers that shall be serialized with >>
Martin Quinson [Fri, 11 Feb 2022 09:24:40 +0000 (10:24 +0100)]
Pass the depends() from the observer to the mc::Transition for CommWait, Send and Recv
Martin Quinson [Fri, 11 Feb 2022 00:48:24 +0000 (01:48 +0100)]
Big bang in MC: app's observers are serialized, to become transitions in checker
Instead of interacting with the observers over the network, we now
transfer over the wire (a simplified copy of) the observer to the
checker.
This was necessary because the lifetime of the Observer (or of its
components) was sometimes too short: it happened that the Actor
refered to by the Observer was not existing anymore at the end of the
simulation when the depend relation was evaluated. Or something like
that, I'm not sure.
Another argument for this change was that UDPOR reduction sometimes
need to evaluate the dependency between transitions that are not in
the same history (in the same run of the application), so we really
need to carry the transition over to let them live in the checker.
Note that we are not copying every information of the observer over,
only the ones that are relevant to the model-checker.
Finally, this change is still ongoing:
- not all observers are serialized over the wire yet
- the depends() are not implemented in the Transition yet
- the network protocol is utterly inefficient, and we probably need
to move to FlatBuffer or something like that.
- a lot of dead code remains
Sorry for the mess, it's progressing rather slowly...
Arnaud Giersch [Thu, 10 Feb 2022 10:54:05 +0000 (11:54 +0100)]
[pvs] Try to fix exclusions for parserPromela.tab.cacc.
Arnaud Giersch [Thu, 10 Feb 2022 09:38:32 +0000 (10:38 +0100)]
[pvs] Don't let members uninitialized.
Arnaud Giersch [Thu, 10 Feb 2022 08:29:03 +0000 (09:29 +0100)]
Another pointer-to-const.
Arnaud Giersch [Wed, 9 Feb 2022 12:55:02 +0000 (13:55 +0100)]
pointer2const4sonar
Arnaud Giersch [Wed, 9 Feb 2022 12:12:52 +0000 (13:12 +0100)]
Forward all the parameters to the observer.
Arnaud Giersch [Tue, 8 Feb 2022 21:46:37 +0000 (22:46 +0100)]
Fix memory leak with ns3 routing tables.
Arnaud Giersch [Tue, 8 Feb 2022 15:50:32 +0000 (16:50 +0100)]
Leak--.
Arnaud Giersch [Tue, 8 Feb 2022 14:52:52 +0000 (15:52 +0100)]
Avoid shadowed declarations.
Arnaud Giersch [Tue, 8 Feb 2022 14:48:04 +0000 (15:48 +0100)]
Kill useless call to get_init().
Arnaud Giersch [Mon, 7 Feb 2022 16:00:18 +0000 (17:00 +0100)]
Update .mailmap [ci-skip].
Arnaud Giersch [Wed, 2 Feb 2022 11:21:13 +0000 (12:21 +0100)]
Reduce scope for variables.
SUTER Frederic [Tue, 8 Feb 2022 10:57:07 +0000 (11:57 +0100)]
simplify calls to CommImpl::isend and CommImpl::irecv
SUTER Frederic [Tue, 8 Feb 2022 10:12:05 +0000 (11:12 +0100)]
[sonar] constify
Martin Quinson [Mon, 7 Feb 2022 14:15:24 +0000 (15:15 +0100)]
Fast path: don't check the dependency between null observers: it's dependent
Martin Quinson [Mon, 7 Feb 2022 11:10:06 +0000 (12:10 +0100)]
Unify the way we count expended states between checkers