An error when using model checker on raft model

[yn...@ucsc.edu]

Hi,

when I ran the model checker against the raft model, I got this error ( I got the exactly same error when I use model checker on a new model I implemented).  Base on log, I figure it's because model checker ran out of the memory.  Does anyone know how to solve this problem?

NideMacBook-Air:runway-compiler niyuanjiang$ ./bin/main.js check -a ../runway-model-raft/raft.model

Checked 650, expanded 100 (15% of checked)
.....
.....

Checked 509599, expanded 87500 (17% of checked)

<--- Last few GCs --->

[4223:0x102804c00]  7259514 ms: Mark-sweep 1895.6 (1984.1) -> 1895.6 (1984.1) MB, 190.1 / 0.0 ms  allocation failure GC in old space requested

[4223:0x102804c00]  7259654 ms: Mark-sweep 1895.6 (1984.1) -> 1895.6 (1954.1) MB, 137.9 / 0.0 ms  last resort gc

[4223:0x102804c00]  7259805 ms: Mark-sweep 1895.6 (1954.1) -> 1895.5 (1954.1) MB, 150.4 / 0.0 ms  last resort gc

<--- JS stacktrace --->

==== JS stack trace =========================================

    2: arguments adaptor frame: 3->2

Security context: 0x1b25f7fc0d31 <JS Object>

    3: InnerArrayForEach(aka InnerArrayForEach) [native array.js:~777] [pc=0x213f99a8efa2](this=0x1b25f7f04311 <undefined>,bk=0x1ef89992b251 <JS Function loops.forEach (SharedFunctionInfo 0x372d32c5a229)>,bl=0x1b25f7f04311 <undefined>,q=0x372d32ca0b21 <JS Array[1]>,r=1)

    4: forEach [native array.js:~795] [pc=0x213f99a66e14](this=0x372d32ca0b21 <JS Array[1...

FATAL ERROR: CALL_AND_RETRY_LAST Allocation failed - JavaScript heap out of memory

 1: node::Abort() [/usr/local/bin/node]

 2: node::FatalException(v8::Isolate*, v8::Local<v8::Value>, v8::Local<v8::Message>) [/usr/local/bin/node]

 3: v8::Utils::ReportOOMFailure(char const*, bool) [/usr/local/bin/node]

 4: v8::internal::V8::FatalProcessOutOfMemory(char const*, bool) [/usr/local/bin/node]

 5: v8::internal::Factory::NewFixedArray(int, v8::internal::PretenureFlag) [/usr/local/bin/node]

 6: v8::internal::TypeFeedbackVector::New(v8::internal::Isolate*, v8::internal::Handle<v8::internal::TypeFeedbackMetadata>) [/usr/local/bin/node]

 7: v8::internal::SharedFunctionInfo::FindOrCreateLiterals(v8::internal::Handle<v8::internal::SharedFunctionInfo>, v8::internal::Handle<v8::internal::Context>) [/usr/local/bin/node]

 8: v8::internal::JSFunction::EnsureLiterals(v8::internal::Handle<v8::internal::JSFunction>) [/usr/local/bin/node]

 9: v8::internal::Compiler::Compile(v8::internal::Handle<v8::internal::JSFunction>, v8::internal::Compiler::ClearExceptionFlag) [/usr/local/bin/node]

10: v8::internal::Runtime_CompileLazy(int, v8::internal::Object**, v8::internal::Isolate*) [/usr/local/bin/node]

11: 0x213f998063a7

12: 0x213f9980675a

13: 0x213f99807e55

14: 0x213f99a8efa2

15: 0x213f99a66e14

Abort trap: 6

[Diego Ongaro]

Hey and sorry for the delay,

That certainly shows the model checker running out of memory, and it's because the current model checker is extremely basic. Unfortunately, I don't have a great solution. You could try:

1) Increasing the Javascript heap size, though O(1) probably won't win against O(2^n);

2) Limiting the parameters of your model to something extremely small;

3) Porting your model over to a more mature model checker; or

4) Doing a bunch of work on Runway to compile Runway models down to a different model checker.

The last one would be ideal, but it'd also take some significant effort. :/

Best,

Diego

--
You received this message because you are subscribed to the Google Groups "runway-dev" group.
To unsubscribe from this group and stop receiving emails from it, send an email to runway-dev+unsubscribe@googlegroups.com.
To post to this group, send email to runwa...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/runway-dev/54282c79-4a69-41d4-a887-4d6ce9613368%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.