Luke Simon | 27 Jun 2007 21:20
Picon

Domain size and scalability of equality

I am currently running to scalability issues with the equality predicate on a domain 32 bits in size (2^32).  Since domains are a fixed size, I have to choose a fixed size that is large enough for analyzing any target application.  However, even for a domain size of 2^32, the initialization of the equality predicate does not terminate.  When using libbuddy, it segfaults.  When using the pure Java BDD solver, it simply runs out of memory.


For now, I am going to scale back to using a fixed domain size of 2^20, and just hope that I don't run into an application that needs  a larger domain.

-------------------------------------------------------------------------
This SF.net email is sponsored by DB2 Express
Download DB2 Express C - the FREE version of DB2 express and take
control of your XML. No limits. Just data. Click to get it now.
http://sourceforge.net/powerbar/db2/
_______________________________________________
bddbddb-devel mailing list
bddbddb-devel <at> lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/bddbddb-devel
John Whaley | 12 Aug 2007 03:48
Picon

Re: Domain size and scalability of equality

Hi Luke,

Equality predicates of any reasonable size *must* have their BDD
domains interleaved.  You can set a variable order using the
.bddvarorder directive in the Datalog file or -Dbddvarorder= on the
command line.

-John

On 6/27/07, Luke Simon <luke.simon <at> gmail.com> wrote:
> I am currently running to scalability issues with the equality predicate on
> a domain 32 bits in size (2^32).  Since domains are a fixed size, I have to
> choose a fixed size that is large enough for analyzing any target
> application.  However, even for a domain size of 2^32, the initialization of
> the equality predicate does not terminate.  When using libbuddy, it
> segfaults.  When using the pure Java BDD solver, it simply runs out of
> memory.
>
>
> For now, I am going to scale back to using a fixed domain size of 2^20, and
> just hope that I don't run into an application that needs  a larger domain.
>
> -------------------------------------------------------------------------
> This SF.net email is sponsored by DB2 Express
> Download DB2 Express C - the FREE version of DB2 express and take
> control of your XML. No limits. Just data. Click to get it now.
> http://sourceforge.net/powerbar/db2/
> _______________________________________________
> bddbddb-devel mailing list
> bddbddb-devel <at> lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/bddbddb-devel
>
>

-------------------------------------------------------------------------
This SF.net email is sponsored by: Splunk Inc.
Still grepping through log files to find problems?  Stop.
Now Search log events and configuration files using AJAX and a browser.
Download your FREE copy of Splunk now >>  http://get.splunk.com/

Gmane