Marion Guthmuller [Mon, 24 Feb 2014 17:39:18 +0000 (18:39 +0100)]
model-checker : use separate configuration flags for comm determinism and send determinism detection
Marion Guthmuller [Mon, 24 Feb 2014 16:03:37 +0000 (17:03 +0100)]
model-checker : check if action not NULL before using it
Gabriel Corona [Mon, 24 Feb 2014 08:27:07 +0000 (09:27 +0100)]
Merge branch 'mc-perf' into mc
Gabriel Corona [Mon, 24 Feb 2014 08:27:01 +0000 (09:27 +0100)]
Fix compilation
Gabriel Corona [Fri, 21 Feb 2014 14:21:41 +0000 (15:21 +0100)]
[mc] Avoid resolving TLS over and over again
Gabriel Corona [Fri, 21 Feb 2014 09:04:09 +0000 (10:04 +0100)]
[mc] Merge add_compared_pointers and already_compared_pointers into add_compared_pointers
Avoid doing the binary search twice.
Gabriel Corona [Thu, 20 Feb 2014 11:26:24 +0000 (12:26 +0100)]
[mc] Avoid (slow) type lookups by name or ID (xbt_dict_get_or_null)
Gabriel Corona [Thu, 20 Feb 2014 10:56:22 +0000 (11:56 +0100)]
[mc] Move mc_find_frame_base in mc_dwarf.c where it belongs
Gabriel Corona [Thu, 20 Feb 2014 10:54:46 +0000 (11:54 +0100)]
[mc] Use resolved addresses in entry.low_pc and entry.high_pc
Gabriel Corona [Thu, 20 Feb 2014 10:41:03 +0000 (11:41 +0100)]
[mc] Use resolved addresses in frame->low_pc and frame->high_pc
Gabriel Corona [Tue, 18 Feb 2014 10:38:14 +0000 (11:38 +0100)]
[mc] Do not waste time calling libunwind get_proc_name in the hot spots
In typical executions, nearly 50% of the time was spent in libunwind
get_proc_name.
The algorithm to find the function for a given IP (instruction
pointer) was:
(proc_name, offset) = get_proc_name(ip) // Slow!
dwarf_ip = ip - offset
function = functions_by_name[proc_name]
We added a structure mapping IP ranges to functions and the algorithm
is now:
function = functions_by_ip[ip]
Instead of relying on libunwind, we use the DWARF information to find
the corresponding DWARF TAG_subprogram DIEs directly.
The secution time on some MPICH tests is nearly halved.
Notes:
* It was necessary to disable the support for inlined_subprograms
which was broken anyway: the inlined_subprogram entries should be
stored as children of their parent subprogram (as a block). We need
to add support for scope blocks inside a suprogram to handle this
correctly.
* Currently the translation between process virtual addresses and
DWARF virtual addresses is handled in many different places. We
should change this to process it only when parsing the DWARF DIEs
and be done with it.
Marion Guthmuller [Tue, 18 Feb 2014 14:41:16 +0000 (15:41 +0100)]
model-checker : conflit
Marion Guthmuller [Tue, 18 Feb 2014 14:33:43 +0000 (15:33 +0100)]
model-checker : minor fix
Marion Guthmuller [Tue, 18 Feb 2014 14:33:13 +0000 (15:33 +0100)]
model-checker : new configuration flag for the detection of determinism in communications schemes
Marion Guthmuller [Tue, 18 Feb 2014 14:02:56 +0000 (15:02 +0100)]
model-checker : remove or comment some printf
Marion Guthmuller [Tue, 18 Feb 2014 13:46:55 +0000 (14:46 +0100)]
model-checker : fix comm destroy for send detached and MC enabled
Marion Guthmuller [Tue, 18 Feb 2014 13:44:13 +0000 (14:44 +0100)]
model-checker : try to fix the model-checker in case of send detached
Marion Guthmuller [Tue, 18 Feb 2014 13:26:28 +0000 (14:26 +0100)]
model-checker : wait with timeout is always dependant with another transition
Marion Guthmuller [Tue, 18 Feb 2014 13:19:01 +0000 (14:19 +0100)]
fix debug log
Marion Guthmuller [Tue, 18 Feb 2014 13:16:27 +0000 (14:16 +0100)]
model-checker : use MC_assert instead of assert for the verification of mpich3 integrated tests
Gabriel Corona [Tue, 18 Feb 2014 10:40:32 +0000 (11:40 +0100)]
[mc] Avoid parsing /proc/self/maps if possible (continued)
Gabriel Corona [Mon, 17 Feb 2014 14:17:23 +0000 (15:17 +0100)]
[mc] Fix get_object_info
Some part of the RW segment was not included (the .bss).
Gabriel Corona [Mon, 17 Feb 2014 13:27:57 +0000 (14:27 +0100)]
[mc] Avoid parsing /proc/self/maps if possible
Gabriel Corona [Fri, 14 Feb 2014 12:43:05 +0000 (13:43 +0100)]
[mc] Doxygen mc_dpor.c (and some mc_liveness.c)
Gabriel Corona [Fri, 14 Feb 2014 10:59:01 +0000 (11:59 +0100)]
[mc] Disable MC_DEBUG (enabled by mistake)
Gabriel Corona [Tue, 11 Feb 2014 12:38:04 +0000 (13:38 +0100)]
[mc] Make usage of state hash a runtime parameter (instead of compile-time)
"off" by default.
Gabriel Corona [Mon, 10 Feb 2014 14:02:13 +0000 (15:02 +0100)]
[mc] Code for evaluation of the impact of the hash
Generate log for evaluating the result of the test:
* true positive;
* true negative;
* false negative (there must not be any of them);
* false positive (should be minimised).
Gabriel Corona [Mon, 10 Feb 2014 12:39:09 +0000 (13:39 +0100)]
[mc] Cache stack unwindinwg
Too much time is spent in libunwind.
Gabriel Corona [Mon, 10 Feb 2014 10:49:07 +0000 (11:49 +0100)]
[mc] Fix broken type lookup code
Gabriel Corona [Mon, 10 Feb 2014 10:15:29 +0000 (11:15 +0100)]
Merge branch 'mc' into mc-perf
Gabriel Corona [Mon, 10 Feb 2014 10:13:37 +0000 (11:13 +0100)]
[mc] Remove useless code (get SP register)
Gabriel Corona [Mon, 10 Feb 2014 10:11:09 +0000 (11:11 +0100)]
[mc] Use optimized local implementation of libuwind (UNW_LOCAL_ONLY)
Gabriel Corona [Mon, 10 Feb 2014 09:31:50 +0000 (10:31 +0100)]
[mc] Restore old behaviour when comparing pointers leading to different segments
Do not terminate the program but assume the state is different.
Gabriel Corona [Fri, 7 Feb 2014 14:44:15 +0000 (15:44 +0100)]
[mc] Fix sefault where a variable has no name
This happen when optimisation is enabled.
As the current code needs a name for the variable, we generate a fake
one. We might want to remove this assumption.
Gabriel Corona [Fri, 7 Feb 2014 12:16:09 +0000 (13:16 +0100)]
Merge branch mc into mc-perf
Gabriel Corona [Fri, 7 Feb 2014 11:45:28 +0000 (12:45 +0100)]
[mc] Split address/location in dw_variable_t (which were in a union)
Gabriel Corona [Fri, 7 Feb 2014 10:56:08 +0000 (11:56 +0100)]
[mc] Fix segfaults when type->name==NULL
Gabriel Corona [Fri, 7 Feb 2014 10:55:50 +0000 (11:55 +0100)]
[mc] Disable communication pattern code (segfault)
Gabriel Corona [Fri, 7 Feb 2014 08:50:09 +0000 (09:50 +0100)]
[mc] Remove dead code for ignoring variables
Gabriel Corona [Fri, 7 Feb 2014 08:25:30 +0000 (09:25 +0100)]
[mc] Remove old hash code
Gabriel Corona [Tue, 4 Feb 2014 13:33:57 +0000 (14:33 +0100)]
[mc] Avoid useless zero-initialisations in the hot spot
Gabriel Corona [Tue, 4 Feb 2014 12:34:53 +0000 (13:34 +0100)]
[mc] Avoid type lookups and calls to get_type_description()
Faster and cache-friendlier.
Gabriel Corona [Tue, 4 Feb 2014 12:00:52 +0000 (13:00 +0100)]
[mc] Pass mc_object_info_t arguiments in many places intead of info->types
Preparation to remove get_type_description() calls which are very
inneficient.
Gabriel Corona [Tue, 4 Feb 2014 10:18:38 +0000 (11:18 +0100)]
[mc] Preprocess type lookup
Avoid looking up the types in the dictionnaries.
Gabriel Corona [Tue, 21 Jan 2014 11:25:30 +0000 (12:25 +0100)]
[mc] Compute a single hash (64 bits) of the current state
This is an attempt to speedup state comparison by using
a very fast first pass.
Compared to previous attempt:
* use a simple 64 bits djb2 hash instead of SHA-1;
* add has much info as possible into the hash;
* do not add anything suspicious;
* it could be used for efficient state comparison
* index for hashtable,
* cache-friendly data-structure.
Gabriel Corona [Tue, 4 Feb 2014 09:18:59 +0000 (10:18 +0100)]
[mc] Remove code for finding an array byte size
This was useless as it was already handled by libdw dwarf_aggregate_size.
Gabriel Corona [Mon, 3 Feb 2014 11:09:25 +0000 (12:09 +0100)]
[mc] Fix broken type in compare_heap_area_with_type
Gabriel Corona [Mon, 20 Jan 2014 14:23:54 +0000 (15:23 +0100)]
[mc] Enforce some assumption about the relationship of the compared areas in compare_areas_with_type
Compare_areas_with_type expects that either :
* both area are in the heap;
* both area are in the current segment R/W segment.
Otherwise, it falls back to comparing pointers.
Changes to code to fail if both areas are not in the same segment
Gabriel Corona [Mon, 20 Jan 2014 13:43:31 +0000 (14:43 +0100)]
[mc] Add comments to compare_areas_with_type
Gabriel Corona [Mon, 20 Jan 2014 12:09:22 +0000 (13:09 +0100)]
[mc] Do not ignore DW_TAG_const_type
Gabriel Corona [Mon, 20 Jan 2014 12:06:07 +0000 (13:06 +0100)]
[mc] In compare_global_variables only compare values in the R/W segment
The algorithme is only relevant if the variable is in the R/W segment
otherwise the resulting pointer will be broken and might result in a
SIGSEV.
This happen if we try to compare a pointer on the .rodata (such as
__FUNCTION__).
Values are supposed to be constant and we do not expect to find
pointers to something which is not reachable by the global variables.
Gabriel Corona [Mon, 20 Jan 2014 10:21:43 +0000 (11:21 +0100)]
[mc] DRY in snapshot_compare
Gabriel Corona [Mon, 20 Jan 2014 09:19:38 +0000 (10:19 +0100)]
[mc] Have a more complete/accurate view of an given object mapping in memory
* Change the terminology (exec/rw instead of text/data)
as we do not have information about the sections but only
about the segments.
* Add information about the read only segment.
Gabriel Corona [Fri, 31 Jan 2014 10:58:07 +0000 (11:58 +0100)]
[mc] Fix element count computation for a givena array dimension
element_count = upper_bound - lower_bound + 1
and not
element_count = upper_bound - lower_bound
Gabriel Corona [Wed, 29 Jan 2014 10:35:04 +0000 (11:35 +0100)]
[mc] Fix handling of location
The handling of member offsets was broken (DW_AT_data_member_location)
and was always 0.
Add support for the class of a given attribute value.
Gabriel Corona [Mon, 20 Jan 2014 09:18:14 +0000 (10:18 +0100)]
[mc] Comment logging in order to fix the unit tests
Marion Guthmuller [Fri, 17 Jan 2014 12:15:58 +0000 (13:15 +0100)]
Merge remote-tracking branch 'origin/libdw2'
Gabriel Corona [Fri, 17 Jan 2014 11:12:05 +0000 (12:12 +0100)]
[mc] Add DW_TAG_formal_parameter as variables in the frames
Gabriel Corona [Fri, 17 Jan 2014 10:30:07 +0000 (11:30 +0100)]
[mc] Use literal values in DWARF constant to name mappings
Gabriel Corona [Thu, 16 Jan 2014 14:57:52 +0000 (15:57 +0100)]
[mc] Cleanup mc_dwarf.c
Gabriel Corona [Fri, 17 Jan 2014 10:16:51 +0000 (11:16 +0100)]
[mc] Remove useless argument in MC_dwarf_at_location
Gabriel Corona [Thu, 16 Jan 2014 14:50:21 +0000 (15:50 +0100)]
[mc] Add comments/doxygen
Gabriel Corona [Thu, 16 Jan 2014 14:14:00 +0000 (15:14 +0100)]
[mc] Free memory for object_info
Gabriel Corona [Thu, 16 Jan 2014 12:08:00 +0000 (13:08 +0100)]
[mc] Remove objdump code
Gabriel Corona [Thu, 16 Jan 2014 11:58:06 +0000 (12:58 +0100)]
[mc] Remove code for location of .plt and .got.plt
This code was not used anyway. If necessary a new solution which do
not depend on objdump should be used.
Gabriel Corona [Thu, 16 Jan 2014 10:50:23 +0000 (11:50 +0100)]
[mc] Use libdw for location list
Gabriel Corona [Mon, 13 Jan 2014 10:56:17 +0000 (11:56 +0100)]
[mc] Use libdw for functions and local variables
Gabriel Corona [Fri, 10 Jan 2014 13:40:22 +0000 (14:40 +0100)]
[mc] Use libdw for global variables
Gabriel Corona [Fri, 10 Jan 2014 14:42:51 +0000 (15:42 +0100)]
[mc] Deduplicate address location resolution in MC_dwarf_resolve_location()
Gabriel Corona [Fri, 10 Jan 2014 13:31:41 +0000 (14:31 +0100)]
[mc] Remove MC_dwarf_tag_type()
Gabriel Corona [Fri, 10 Jan 2014 13:24:16 +0000 (14:24 +0100)]
[mc] Add dwarf_global field to dw_variable_t
It is a better (but not perfect) identifier for a entry.
Gabriel Corona [Mon, 6 Jan 2014 10:21:02 +0000 (11:21 +0100)]
[mc] libdwarf integration for types
Gabriel Corona [Mon, 6 Jan 2014 11:20:56 +0000 (12:20 +0100)]
[mc] Use DWARF constants for type tags
Gabriel Corona [Mon, 23 Dec 2013 13:36:07 +0000 (14:36 +0100)]
[mc] Link against libdw
Gabriel Corona [Fri, 17 Jan 2014 09:20:06 +0000 (10:20 +0100)]
[mc] Fix warnings
Marion Guthmuller [Thu, 16 Jan 2014 14:24:03 +0000 (15:24 +0100)]
model-checker : first steps for the study of MPI communications patterns
Gabriel Corona [Tue, 7 Jan 2014 09:33:11 +0000 (10:33 +0100)]
[mc] Remove type DW_TAG_enumerator type (because it is not a type)
Gabriel Corona [Mon, 6 Jan 2014 14:01:45 +0000 (15:01 +0100)]
[mc] Split byte_size and element_count in mc_object_info_t
Gabriel Corona [Mon, 6 Jan 2014 09:35:52 +0000 (10:35 +0100)]
[mc] Remove spurious return in MC_find_object_address
Gabriel Corona [Thu, 9 Jan 2014 13:30:38 +0000 (14:30 +0100)]
[mc] Add comments
Gabriel Corona [Fri, 3 Jan 2014 11:02:17 +0000 (12:02 +0100)]
[mc] Restore lightweight MC initialisation procedure
Gabriel Corona [Thu, 2 Jan 2014 14:22:23 +0000 (15:22 +0100)]
[mc] Cleanup mc_object_info_t code
Gabriel Corona [Thu, 2 Jan 2014 13:57:46 +0000 (14:57 +0100)]
[mv] Remove global {start,end}_{plt,got}_{libsimgrid,binary}
Gabriel Corona [Thu, 2 Jan 2014 12:57:16 +0000 (13:57 +0100)]
[mc] Add plt/got in mc_object_info_t
Gabriel Corona [Tue, 24 Dec 2013 14:07:43 +0000 (15:07 +0100)]
[mc] Move start_text, start_data, start_bss into mc_object_info_t
Gabriel Corona [Tue, 24 Dec 2013 13:25:34 +0000 (14:25 +0100)]
[mc] Include ELF file name in object_info_t
Gabriel Corona [Thu, 2 Jan 2014 10:01:12 +0000 (11:01 +0100)]
[mc] Remvove mc_{global_variables,local_variables,variables_type}_{libsimgrid,binary}
Gabriel Corona [Thu, 2 Jan 2014 09:49:24 +0000 (10:49 +0100)]
[mc] Do not use mc_{global_variables,local_variables,variables_type}_{libsimgrid,binary}
Gabriel Corona [Thu, 2 Jan 2014 08:52:19 +0000 (09:52 +0100)]
[mc] Refactor, group some informations about a given ELF in mc_object_info_t
Gabriel Corona [Thu, 2 Jan 2014 13:50:52 +0000 (14:50 +0100)]
[mc] Use LANG=C when calling objdump
The output of objdump change with the locale and the parser fails with some locales.
Conflicts:
src/mc/mc_checkpoint.c
Gabriel Corona [Tue, 24 Dec 2013 11:04:04 +0000 (12:04 +0100)]
[mc] Add some documentation to the MC DWARF code
Gabriel Corona [Mon, 6 Jan 2014 13:58:48 +0000 (14:58 +0100)]
[mc] Fix bug in recurive call of compare_heap_area_with_type
When comparing arrays, the number of elements of the array was passed instead of the size of the elements.
Gabriel Corona [Fri, 20 Dec 2013 11:58:13 +0000 (12:58 +0100)]
[mc] Fix bug when parsing /proc/self/maps
Sometimes, the heap is not found by the MC :
* the MC expects the heap to be anonymous/unlabelled in
/proc/self/maps;
* the heap may be labelled as as [stack:$tid] in /proc/self/maps at
some instants of the execution of the program because the tasks
stacks are allocated on the heap.
Gabriel Corona [Fri, 20 Dec 2013 10:07:01 +0000 (11:07 +0100)]
Arnaud Giersch [Fri, 8 Nov 2013 22:55:41 +0000 (23:55 +0100)]
Release version 3.10-rc2.
Arnaud Giersch [Fri, 8 Nov 2013 22:53:10 +0000 (23:53 +0100)]
This part is not relevant anymore.
Arnaud Giersch [Fri, 8 Nov 2013 22:04:03 +0000 (23:04 +0100)]
Give smpiff the directory to libf2c.
(cherry picked from commit
1848d40fafafab07f8c798116d5c507065f4c97b)
Arnaud Giersch [Fri, 8 Nov 2013 22:03:10 +0000 (23:03 +0100)]
Don't add include directories when f77 support is disabled.
(cherry picked from commit
482244d2827841bb565348470beb8167c7558337)
Arnaud Giersch [Fri, 8 Nov 2013 16:49:41 +0000 (17:49 +0100)]
Try to fix temp file creation.
(cherry picked from commit
0be4d91dea4f9aeb5e9e298dc579d4ba2b03a2b7)
Augustin Degomme [Fri, 8 Nov 2013 00:12:20 +0000 (01:12 +0100)]
be a little more tricky and hopefully more portable
(cherry picked from commit
3e7047f7353ca1853d3eb5415264714a0315a8d4)