MRMC with huge models
Dear all, I'm a newbie in model checking but for my PhD project a great option is model analysis. In project a huge CTMC model (.tra) with 797382144 STATES and 64470375837 TRANSITIONS is generated. First I noticed that MRMC "only" requests 3GB RAM which seems to be filled. In that process a core dump is generated. I noticed that MRMC seems not to load all transitions or eventually represents the transition count in a wrong way (may be a variable overflow). Do you have some experience with analysing such big models? Are there some restrictions by MRMC ? Best Martin Groessl ----------------------------------------------------- Technical University of Kaiserslautern Department of ComputerScience 67653 Kaiserslautern,Germany Email: groessl@informatik.uni-kl.de
Dear Martin,
... a huge CTMC model (.tra) with 797382144 STATES and 64470375837 TRANSITIONS is generated. First I noticed that MRMC "only" requests 3GB RAM which seems to be filled. In that process a core dump is generated. I noticed that MRMC seems not to load all transitions or eventually represents the transition count in a wrong way (may be a variable overflow).
I think that is it: The number of transitions is almost 2^36, but is stored by MRMC in an integer variable. Most C compilers assign 32 bits for this type. MRMC unfortunately does not check in the first two lines whether the number of states or the number of transitions exceed the bounds; the lines that contain the transitions themselves are checked a bit more thoroughly. Before requesting space for all the transitions, MRMC makes a first pass through the file to find the out-degree of each state. These out-degrees are stored in an array of integers; in your case, that array would be 797382144 * 4 B = 2,97 GB large. After the first pass through the file, MRMC allocates space for the actual transitions: initially 12 B per transition, which will later be extended by another 4 B for the so-called backsets. However, it only allocates space for 45866397 transitions (= 64470375837 modulo 2^32), i. e. 525 KB. When this space is full, MRMC will (without checking further) store remaining transitions outside its assigned memory, which then leads to the core dump. I think this is why MRMC uses (a bit more than) 3 GB before crashing. Kind regards, David N. Jansen.
Dear David, many thanks for you reply.
I think that is it: The number of transitions is almost 2^36, but is stored by MRMC in an integer variable. Most C compilers assign 32 bits for this type.
I noticed that and adapted the variable types from int to long.
Before requesting space for all the transitions, MRMC makes a first pass through the file to find the out-degree of each state. These out-degrees are stored in an array of integers; in your case, that array would be 797382144 * 4 B = 2,97 GB large.
That size (2,97 GB) corresponds to what htop shows.
After the first pass through the file, MRMC allocates space for the actual transitions: initially 12 B per transition, which will later be extended by another 4 B for the so-called backsets. However, it only allocates space for 45866397 transitions (= 64470375837 modulo 2^32), i. e. 525 KB.
Do you think allocating more space is feasible in (case it's physical available).
When this space is full, MRMC will (without checking further) store remaining transitions outside its assigned memory, which then leads to the core dump. I think this is why MRMC uses (a bit more than) 3 GB before crashing.
I'll try to find a work around for that. Best regards Martin Am Mi 19.11.2014 10:07 schrieb David N. Jansen <dnjansen@cs.ru.nl>:
Dear Martin,
... a huge CTMC model (.tra) with 797382144 STATES and 64470375837 TRANSITIONS is generated. First I noticed that MRMC "only" requests 3GB RAM which seems to be filled. In that process a core dump is generated. I noticed that MRMC seems not to load all transitions or eventually represents the transition count in a wrong way (may be a variable overflow).
I think that is it: The number of transitions is almost 2^36, but is stored by MRMC in an integer variable. Most C compilers assign 32 bits for this type. MRMC unfortunately does not check in the first two lines whether the number of states or the number of transitions exceed the bounds; the lines that contain the transitions themselves are checked a bit more thoroughly.
Before requesting space for all the transitions, MRMC makes a first pass through the file to find the out-degree of each state. These out-degrees are stored in an array of integers; in your case, that array would be 797382144 * 4 B = 2,97 GB large. After the first pass through the file, MRMC allocates space for the actual transitions: initially 12 B per transition, which will later be extended by another 4 B for the so-called backsets. However, it only allocates space for 45866397 transitions (= 64470375837 modulo 2^32), i. e. 525 KB. When this space is full, MRMC will (without checking further) store remaining transitions outside its assigned memory, which then leads to the core dump. I think this is why MRMC uses (a bit more than) 3 GB before crashing.
Kind regards, David N. Jansen.
Dear Martin,
I think that is it: The number of transitions is almost 2^36, but is stored by MRMC in an integer variable. Most C compilers assign 32 bits for this type.
I noticed that and adapted the variable types from int to long.
I propose that, if you adapt the code, you ask for access to the svn repository. I cannot grant it to you, but somebody at RWTH Aachen should be able to do so. While the responsibles were very reluctant to grant write access, at least they can create a branch for you.
After the first pass through the file, MRMC allocates space for the actual transitions: initially 12 B per transition, which will later be extended by another 4 B for the so-called backsets. However, it only allocates space for 45866397 transitions (= 64470375837 modulo 2^32), i. e. 525 KB.
Do you think allocating more space is feasible in (case it's physical available).
It should be possible, as malloc() and calloc() have parameters of type size_t (which is typedef'd to be unsigned long in many C compilers). Of course, you will also have to change the types of the relevant calculations to size_t. The function allocate_sparse_matrix_ncolse() in src/storage/sparse.c will allocate one big array for all transitions and should use size_t. The function set_mtx_val_ncolse() in the same file updates the backset or the backpointer, allocated a separate, smaller chunks of memory. Probably it is enough to use int here, but it is more consistent to use size_t as well.
When this space is full, MRMC will (without checking further) store remaining transitions outside its assigned memory, which then leads to the core dump. I think this is why MRMC uses (a bit more than) 3 GB before crashing.
I'll try to find a work around for that.
Please have a close look at the source file src/io/read_tra_file.c. That file reads the transition file and allocates memory. Kind regards, David N. Jansen.
Dear David,
I propose that, if you adapt the code, you ask for access to the svn repository.
Currently I use the stable version which is available via download. In case my experiments work I can send you the tar ball. The MRMC project is clear structured and not big hence this should be an option.
It should be possible, as malloc() and calloc() have parameters of type size_t (which is typedef'd to be unsigned long in many C compilers).
This should hopefully work.
Of course, you will also have to change the types of the relevant calculations to size_t. The function allocate_sparse_matrix_ncolse() in src/storage/sparse.c will allocate one big array for all transitions and should use size_t. The function set_mtx_val_ncolse() in the same file updates the backset or the backpointer, allocated a separate, smaller chunks of memory.
I noticed that but beyond that the structure for sparse have to be adapted; It consists of ints.
Please have a close look at the source file src/io/read_tra_file.c. That file reads the transition file and allocates memory. THX! I already did. :)
Best regards Martin Am Do 20.11.2014 11:53 schrieb David N. Jansen <dnjansen@cs.ru.nl>:
Dear Martin,
I think that is it: The number of transitions is almost 2^36, but is stored by MRMC in an integer variable. Most C compilers assign 32 bits for this type.
I noticed that and adapted the variable types from int to long.
I propose that, if you adapt the code, you ask for access to the svn repository. I cannot grant it to you, but somebody at RWTH Aachen should be able to do so. While the responsibles were very reluctant to grant write access, at least they can create a branch for you.
After the first pass through the file, MRMC allocates space for the actual transitions: initially 12 B per transition, which will later be extended by another 4 B for the so-called backsets. However, it only allocates space for 45866397 transitions (= 64470375837 modulo 2^32), i. e. 525 KB.
Do you think allocating more space is feasible in (case it's physical available).
It should be possible, as malloc() and calloc() have parameters of type size_t (which is typedef'd to be unsigned long in many C compilers). Of course, you will also have to change the types of the relevant calculations to size_t. The function allocate_sparse_matrix_ncolse() in src/storage/sparse.c will allocate one big array for all transitions and should use size_t. The function set_mtx_val_ncolse() in the same file updates the backset or the backpointer, allocated a separate, smaller chunks of memory. Probably it is enough to use int here, but it is more consistent to use size_t as well.
When this space is full, MRMC will (without checking further) store remaining transitions outside its assigned memory, which then leads to the core dump. I think this is why MRMC uses (a bit more than) 3 GB before crashing.
I'll try to find a work around for that.
Please have a close look at the source file src/io/read_tra_file.c. That file reads the transition file and allocates memory.
Kind regards, David N. Jansen.
participants (2)
-
David N. Jansen -
Martin Groessl