Chers collègues,
La prochaine session du séminaire Performance et Généricité du LRDE
(Laboratoire de Recherche et Développement de l'EPITA) aura lieu le
Mercredi 13 novembre 2013 (11h--12h30), Salle Lα du LRDE.
Au programme:
* 11h-12h30: Address & Thread Sanitizer in GCC: Etat Actuel et Orientation Future
-- Dodji Seketeli, Red Hat
http://gcc.gnu.org
Address & Thread sanitizer sont des outils destinés à détecter les
erreurs d'accès à la mémoire ainsi que les erreurs d'accès concurrents
en environnement multi-threads.
Ces outils sont constitués de deux parties logiques distinctes: une
partie instrumentant le code généré de manière statique, et un
environnement d'exécution.
Cet exposé présente l'implémentation de Address & Thread Sanitizer dans
GCC, les principes de fonctionnement de l'environnement d'exécution de
ces deux outils ainsi que les futures directions du projet.
-- Dodji Seketeli est ingénieur dans l'équipe Tools de Red Hat. Il
travaille sur la suite des compilateurs GNU, principalement sur les
compilateurs C et C++. Pendant son temps libre, lorsqu'il ne joue pas
avec son épouse et ses enfants, il maintient Nemiver, le debuggeur
graphique du projet d'environnement de bureau libre GNOME. En dehors des
logiciels libres, il s'intéresse aux arts martiaux et à l'histoire.
Pour plus de renseignements, consultez http://seminaire.lrde.epita.fr/.
L'entrée du séminaire est libre. Merci de bien vouloir diffuser cette
information le plus largement possible.
--
Akim Demaille
Akim.Demaille(a)lrde.epita.fr
_______________________________________________
Seminaire mailing list
Seminaire(a)lrde.epita.fr
https://lists.lrde.epita.fr/listinfo/seminaire
We are pleased to inform you that the following paper has been accepted in the 19th International
Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR). Please find the
title and abstract below.
Title and corresponding authors:
"Three SCC-based Emptiness Checks for Generalized Büchi Automata"
E. Renault(1), A. Duret-Lutz(1), F. Kordon(2), and D. Poitrenaud(2)
(1) LRDE-EPITA, www.lrde.epita.fr
(2) UPMC-LIP6, www.lip6.fr
Abstract:
The automata-theoretic approach for the verification of linear time
properties involves checking the emptiness of a Büchi automaton.
However generalized Büchi automata, with multiple acceptance sets,
are preferred when verifying under weak fairness hypotheses.
Existing emptiness checks for which the complexity is independent of
the number of acceptance sets are all based on the enumeration of
Strongly Connected Components (SCCs).
In this paper, we review the state of the art SCC enumeration
algorithms to study how they can be turned into emptiness
checks. This leads us to define two new emptiness check algorithms
(one of them based on the Union Find data structure),
introduce new optimizations, and show that one of these can be of
benefit to a classic SCCs enumeration algorithm. We have
implemented all these variants to compare their relative
performances and the overhead induced by the emptiness check
compared to the corresponding SCCs enumeration algorithm.
Our experiments shows that these three algorithms are comparable.
I'm very pleased to announce the release of Spot 1.2.
Spot is a model-checking library developed collaboratively by LRDE
and LIP6. It provides algorithms and data structures to implement
the automata-theoretic approach to LTL model checking.
This release contains several new features (summarized below), but the
most notable are the interface with ltl2dstar (i.e., Spot can read
deterministic Rabin and Streett automata and convert them into Büchi
automata) and algorithms for minimizing deterministic TGBA or BA using
a SAT-solver.
You can find the new release here:
http://spot.lip6.fr/dl/spot-1.2.tar.gz
Please report any issue to <spot(a)lrde.epita.fr>.
New in spot 1.2 (2013-10-01)
* Changes to command-line tools:
- ltlcross has a new option --color to color its output. It is
enabled by default when the output is a terminal.
- ltlcross will give an example of infinite word accepted by the
two automata when the product between a positive automaton and a
negative automaton is non-empty.
- ltlcross can now read the Rabin and Streett automata output by
ltl2dstar. This type of output should be specified using '%D':
ltlcross 'ltl2dstar --ltl2nba=spin:path/to/ltl2tgba@-s %L %D'
However because Spot only supports Büchi acceptance, these Rabin
and Streett automata are immediately converted to TGBAs before
further processing by ltlcross. This is still interesting to
search for bugs in translators to Rabin or Streett automata, but
the statistics (of the resulting TGBAs) might not be very relevant.
- When ltlcross obtains a deterministic automaton from a
translator it will now complement this automaton to perform
additional intersection checks. This is complementation is done
only for deterministic automata (because that is cheap) and can
be disabled with --no-complement.
- To help with debugging problems detected by ltlcross, the
environment variables SPOT_TMPDIR and SPOT_TMPKEEP control where
temporary files are created and if they should be erased. Read
the man page of ltlcross for details.
- There is a new command, named dstar2tgba, that converts a
deterministic Rabin or Streett automaton (expressed in the
output format of ltl2dstar) into a TGBA, BA or Monitor.
In the case of Rabin acceptance, the conversion will output a
deterministic Büchi automaton if one such automaton exist. Even
if no such automaton exists, the conversion will actually
preserves the determinism of any SCC that can be kept
deterministic.
In the case of Streett acceptance, the conversion produces
non-deterministic Büchi automata with Generalized acceptance.
These are then degeneralized if requested.
See http://spot.lip6.fr/userdoc/dstar2tgba.html for some
examples, and the man page for more reference.
- The %S escape sequence used by ltl2tgba --stats to display the
number of SCCs in the output automaton has been renamed to %c.
This makes it more homogeneous with the --stats option of the
new dstar2tgba command.
Additionally, the %p escape can now be used to show whether the
output automaton is complete, and the %r escape will give the
number of seconds spent building the output automaton (excluding
the time spent parsing the input).
- ltl2tgba, ltl2tgta, and dstar2tgba have a --complete option
to output complete automata.
- ltl2tgba, ltl2tgta, and dstar2tgba can use a SAT-solver to
minimize deterministic automata. Doing so is only needed on
properties that are stronger than obligations (for obligations
our WDBA-minimization procedure will return a minimimal
deterministic automaton more efficiently) and is disabled by
default. See the spot-x(7) man page for documentation about the
related options: sat-minimize, sat-states, sat-acc, state-based.
See also http://spot.lip6.fr/userdoc/satmin.html for some
examples.
- ltlfilt, genltl, and randltl now have a --latex option to output
formulas in a way that its easier to embed in a LaTeX document.
Each operator is output as a command such as \U, \F, etc.
doc/tl/spotltl.sty gives one possible definition for each macro.
- ltlfilt, genltl, and randltl have a new --format option to
indicate how to present the output formula, possibly with
information about the input.
- ltlfilt as a new option, --relabel-bool, to abstract independent
Boolean subformulae as if they were atomic propositions.
For instance "a & GF(c | d) & b & X(c | d)" would be rewritten
as "p0 & GF(p1) & Xp1".
* New functions and classes in the library:
- dtba_sat_synthetize(): Use a SAT-solver to build an equivalent
deterministic TBA with a fixed number of states.
- dtba_sat_minimize(), dtba_sat_minimize_dichotomy(): Iterate
dtba_sat_synthetize() to reduce the number of states of a TBA.
- dtgba_sat_synthetize(), dtgba_sat_minimize(),
dtgba_sat_minimize_dichotomy(): Likewise, for deterministic TGBA.
- is_complete(): Check whether a TGBA is complete.
- tgba_complete(): Complete an automaton by adding a sink state
if needed.
- dtgba_complement(): Complement a deterministic TGBA.
- satsolver(): Run an (external) SAT solver, honoring the
SPOT_SATSOLVER environment variable if set.
- tba_determinize(): Run a power-set construction, and attempt
to fix the acceptance simulation to build a deterministic TBA.
- dstar_parse(): Read a Streett or Rabin automaton in
ltl2dstar's format. Note that this format allows only
deterministic automata.
- nra_to_nba(): Convert a (possibly non-deterministic) Rabin
automaton to a non-deterministic Büchi automaton.
- dra_to_ba(): Convert a deterministic Rabin automaton to a Büchi
automaton, preserving acceptance in all SCCs where this is possible.
- nsa_to_tgba(): Convert a (possibly non-deterministic) Streett
automaton to a non-deterministic TGBA.
- dstar_to_tgba(): Convert any automaton returned by dstar_parse()
into a TGBA.
- build_tgba_mask_keep(): Build a masked TGBA that shows only
a subset of states of another TGBA.
- build_tgba_mask_ignore(): Build a masked TGBA that ignore
a subset of states of another TGBA.
- class tgba_proxy: Helps writing on-the-fly algorithms that
delegate most of their methods to the original automaton.
- class bitvect: A dynamic bit vector implementation.
- class word: An infinite word, stored as prefix + cycle, with a
simplify() methods to simplify cycle and prefix in obvious ways.
- class temporary_file: A temporary file. Can be instanciated with
create_tmp_file() or create_open_tmpfile().
- count_state(): Return the number of states of a TGBA. Implement
a couple of specializations for classes where is can be know
without exploration.
- to_latex_string(): Output a formula using LaTeX syntax.
- relabel_bse(): Relabeling of Boolean Sub-Expressions.
Implements ltlfilt's --relabel-bool option describe above.
* Noteworthy internal changes:
- When minimize_obligation() is not given the formula associated
to the input automaton, but that automaton is deterministic, it
can still attempt to call minimize_wdba() and check the correcteness
using dtgba_complement(). This allows dstar2tgba to apply
WDBA-minimization on deterministic Rabin automata.
- tgba_reachable_iterator_depth_first has been redesigned to
effectively perform a DFS. As a consequence, it does not
inherit from tgba_reachable_iterator anymore.
- postproc::set_pref() was used to accept an argument among Any,
Small or Deterministic. These can now be combined with Complete
as Any|Complete, Small|Complete, or Deterministic|Complete.
- operands of n-ary operators (like & and |) are now ordered so
that Boolean terms come first. This speeds up syntactic
implication checks slightly. Also, literals are now sorted
using strverscmp(), so that p5 comes before p12.
- Syntactic implication checks have been generalized slightly
(for instance 'a & b & F(a & b)' is now reduced to 'a & b'
while it was not changed in previous versions).
- All the parsers implemented in Spot now use the same type to
store locations.
- Cleanup of exported symbols
All symbols in the library now have hidden visibility on ELF systems.
Public classes and functions have been marked explicitely for export
with the SPOT_API macro.
During this massive update, some of functions that should not have
been made public in the first place have been moved away so that
they can only be used from the library. Some old of unused
functions have been removed.
removed:
- class loopless_modular_mixed_radix_gray_code
hidden:
- class acc_compl
- class acceptance_convertor
- class bdd_allocator
- class free_list
* Bug fixes:
- Degeneralization was not indempotant on automata with an
accepting initial state that was on a cycle, but without
self-loop.
- Configuring with --enable-optimization would reset the value of
CXXFLAGS.
--
Alexandre Duret-Lutz
