#1 feature request

open
nobody
None
5
2005-11-20
2005-11-20
Ryan Leduc
No

Hello,

I was wondering if you have considered creating a
parallel multithreaded version of your package?

My grad student has used it to verify properties about
Discrete-event systems (represented as automata). He
used it on a syatem at least 10^15 states. It used
about 100MB, but ran for several days without completing.

For large systems, speed rather than memory can be an
issue. I've seen a few papers on parallel version for
BDDs. Such a version could be useful.

Ryan

Discussion

  • Logged In: NO

    Hello Ryan,

    Thanks for your suggestion.
    There are several parallel BDDs packages out there.
    There are no current plan to make BuDDy parallel.
    Do you know what the running time was mostly spent on ? CPU
    or IO ?

     
  • Haim Cohen
    Haim Cohen
    2006-04-29

    Logged In: YES
    user_id=1024352

    Hello Ryan,

    Thanks for your suggestion.
    There are several parallel BDDs packages out there.
    There are no current plan to make BuDDy parallel.
    Do you know what the running time was mostly spent on ? CPU
    or IO ?

    ( now i am logged in ... :-) )

     
  • Ryan Leduc
    Ryan Leduc
    2006-05-01

    Logged In: YES
    user_id=217616

    Hello,

    The program represents a dynamic system as automata. BDDs
    encode state and transition information as well as
    "qualities" about states. One example ran for 26.7 hours,
    220MB memory. As the system has 512MB, I do not believe it
    was swapping. The application implements a fixed point
    operator on the state space. It checks for two properties,
    and trims off states until system satisfies both. This can
    take several iterations. The predicates are reasonable in
    size and complexity at the beginning and the end of an
    iteration, but they can grow to be very complicated and
    large in the middle.

    I would say the time was spent on CPU.

    Ryan

     
  • Haim Cohen
    Haim Cohen
    2006-05-02

    Logged In: YES
    user_id=1024352

    One thing to try is reordering of variables.
    How many BDDs nodes did you reach ?
    BuDDy has different reordering algorithms that can be
    applied if the BDD gets too large. I assume you also started
    with good initial order of variable based on few heuristics.

    Another idea you can try:
    If the "system" doesn't change often but the "qualities"
    are, what you can do is to first build the "system-bdd", try
    some of the reordering algorithms to minimize it, and then
    save the BDD to a file.
    Then ( assuming you were able to minimize the BDD by finding
    a "good" variables order) you can load the "system-BDD" from
    the file (should be fast if you were able to reduce the BDD
    size), and then apply different "qualities". So whenever you
    want to test a new "quality" you may save time by loading a
    smaller "system-BDD".

    Is there any chance to get a copy of your program ?
    You can send it to me by Email and I will not post it in SF
    without your writen permission.
    I want to try it on my machine and see what can be done to
    make BuDDy working for you.

    Thanks,
    Haim

     
  • Ryan Leduc
    Ryan Leduc
    2006-05-08

    Logged In: YES
    user_id=217616

    Hello Haim,

    I sent an e-mail with the source code to the e-mail address
    that you have listed on sourceforge for this project.

    Please let me know if you received it.

    Ryan