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
Martin Quinson [Mon, 7 Feb 2022 09:43:07 +0000 (10:43 +0100)]
Define and use a Transition::to_cstring()
Martin Quinson [Mon, 7 Feb 2022 09:38:40 +0000 (10:38 +0100)]
Move Transition::execute() to State::execute_next()
Martin Quinson [Mon, 7 Feb 2022 09:18:34 +0000 (10:18 +0100)]
Make State::transition_ private
Martin Quinson [Mon, 7 Feb 2022 08:55:04 +0000 (09:55 +0100)]
Move the selection of the next transition to execute to mc::State
Martin Quinson [Mon, 7 Feb 2022 01:34:34 +0000 (02:34 +0100)]
Make Liveness and CommDet more similar to Safety
Martin Quinson [Mon, 7 Feb 2022 01:24:00 +0000 (02:24 +0100)]
MC: inline a function
Martin Quinson [Mon, 7 Feb 2022 00:30:45 +0000 (01:30 +0100)]
Automatize the computation of executed_transitions_
Martin Quinson [Mon, 7 Feb 2022 00:18:19 +0000 (01:18 +0100)]
Move request_execute and request_to_string from api::get() to Transition
Martin Quinson [Sun, 6 Feb 2022 23:56:06 +0000 (00:56 +0100)]
Kill a now unused parameter
Martin Quinson [Sun, 6 Feb 2022 23:51:27 +0000 (00:51 +0100)]
MC: Trade less use of executed_req for more network messages
We go through the network to find the string and dot representations
of transitions even when there is no observer
Martin Quinson [Sun, 6 Feb 2022 22:45:45 +0000 (23:45 +0100)]
MC: simplification: this function shall return a boolean
Its return value was already set to state as a side effect anyway
Martin Quinson [Sun, 6 Feb 2022 22:23:55 +0000 (23:23 +0100)]
Let's use bool for booleans
Martin Quinson [Sun, 6 Feb 2022 22:17:54 +0000 (23:17 +0100)]
MC: Inline and simplify a function
Martin Quinson [Sun, 6 Feb 2022 21:50:36 +0000 (22:50 +0100)]
MC: kill an unused function
Arnaud Giersch [Mon, 7 Feb 2022 11:19:36 +0000 (12:19 +0100)]
Fix error 404 for grey.png with recent jenkins [ci-skip].
SUTER Frederic [Sun, 6 Feb 2022 11:56:37 +0000 (12:56 +0100)]
enforce simcall order as before to check dependencies (Isend, Irecv, Wait)
SUTER Frederic [Sun, 6 Feb 2022 11:43:41 +0000 (12:43 +0100)]
fix isend/irecv to string
SUTER Frederic [Sun, 6 Feb 2022 10:59:09 +0000 (11:59 +0100)]
test and testany are non blocking simcalls
SUTER Frederic [Sat, 5 Feb 2022 18:32:44 +0000 (19:32 +0100)]
kill unused function
Martin Quinson [Sun, 6 Feb 2022 08:35:54 +0000 (09:35 +0100)]
nardin clang (fix clang MC builds)
Martin Quinson [Sun, 6 Feb 2022 00:01:46 +0000 (01:01 +0100)]
MC: rely less on executed_req_ and more on observers
Martin Quinson [Sat, 5 Feb 2022 23:50:45 +0000 (00:50 +0100)]
What about not testing the dependencies of transitions with themselves? bummer
Martin Quinson [Sat, 5 Feb 2022 23:19:02 +0000 (00:19 +0100)]
MC: Kill now unused fields
Martin Quinson [Sat, 5 Feb 2022 22:57:33 +0000 (23:57 +0100)]
Don't compute the dependencies locally in the checker, but through the observers over the network
SUTER Frederic [Sat, 5 Feb 2022 17:56:24 +0000 (18:56 +0100)]
back to normal ... keep progressing towards modern simcalls for all
Martin Quinson [Sat, 5 Feb 2022 14:53:26 +0000 (15:53 +0100)]
MC: isend/irecv are not blocking
Also, add some debug info to the MC exploration
Martin Quinson [Sat, 5 Feb 2022 12:18:30 +0000 (13:18 +0100)]
MC: do not segfault when the logs are activated
Martin Quinson [Fri, 4 Feb 2022 23:52:43 +0000 (00:52 +0100)]
convert more isend/irecv locations to the new simcalls, for compatibility
SUTER Frederic [Fri, 4 Feb 2022 15:54:32 +0000 (16:54 +0100)]
oopsie
SUTER Frederic [Fri, 4 Feb 2022 15:45:11 +0000 (16:45 +0100)]
continue to mess with MC
SUTER Frederic [Fri, 4 Feb 2022 09:25:03 +0000 (10:25 +0100)]
stay with double for payload size (fix 32bit issues?
Martin Quinson [Thu, 3 Feb 2022 21:40:43 +0000 (22:40 +0100)]
specify in the COPYING file that we are LGPL-v2.1-only
Closes: https://framagit.org/simgrid/simgrid/-/issues/101
Martin Quinson [Thu, 3 Feb 2022 21:27:18 +0000 (22:27 +0100)]
preshot sonar (dead code; equality test between double)
SUTER Frederic [Thu, 3 Feb 2022 21:40:29 +0000 (22:40 +0100)]
remove old simcall_comm_test and simcall_comm_testany
SUTER Frederic [Thu, 3 Feb 2022 21:12:16 +0000 (22:12 +0100)]
simcall translation is now useless
Martin Quinson [Thu, 3 Feb 2022 21:25:26 +0000 (21:25 +0000)]
Merge branch 'wifi_rate_zero' into 'master'
zero wifi rate
See merge request simgrid/simgrid!76
SUTER Frederic [Thu, 3 Feb 2022 19:01:09 +0000 (20:01 +0100)]
let SMPI use old simcalls for now
SUTER Frederic [Thu, 3 Feb 2022 16:23:46 +0000 (17:23 +0100)]
make isend and irecv observable (except for irecv in smpi_request.cpp)
SUTER Frederic [Thu, 3 Feb 2022 12:22:47 +0000 (13:22 +0100)]
draft CommI{send,recv}Observer
SUTER Frederic [Wed, 2 Feb 2022 18:32:29 +0000 (19:32 +0100)]
move the code of isend and irecv out of the handler and into CommImpl
Arnaud Giersch [Thu, 3 Feb 2022 14:33:29 +0000 (15:33 +0100)]
Update references to the mailing list.
Arnaud Giersch [Thu, 3 Feb 2022 14:32:45 +0000 (15:32 +0100)]
Merge branch 'stable'
Augustin Degomme [Thu, 3 Feb 2022 10:02:55 +0000 (11:02 +0100)]
add a word in the doc about deploying multiple processes per node in a single line of the hostfile
Augustin Degomme [Thu, 3 Feb 2022 10:00:48 +0000 (11:00 +0100)]
update changelog