-
Notifications
You must be signed in to change notification settings - Fork 105
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Refine, Bisim, Acess I/O error message #15
Comments
I think that Isabelle might not be handling these truncated files.
I know that Isabelle does peek at its old logs to optimise its current runs. It's possible that it doesn't
expect a badly formatted gzip archive.
I'd suggest just removing them, especially if their size is 0, and seeing if Isabelle now makes progress.
Cheers,
Thomas.
On 21/12/16 04:09, AmerTahat wrote:
Hi All,
I am trying to run the Refine, Bisim, and Access tests in my new installation of Sel4 on a dual boot ubuntu 16.04-1 LTL (Xenial Xerus) . I did not get what the error message means, it is too short (please see the example below). If some one can help I will appreciate that a lot.
One note: the first time I ran the tests on my dual boot machine the tests were interrupted due to the small Ubuntu partition size (~50 G) the tests Refine, Bisim, and Acess all have been executing at that time and they failed due to lack of memory and nothing was written. Later I expanded the ubuntu partition, all tests except these three worked (some skipped due dependencies). Moreover, when I
use:
" find $HOME -iname 'Refine.*' -size 0M " it returns :
/home/ssrgv/.isabelle/heaps-ARM-home-ssrgv-Desktop-verification-isabelle/polyml-5.6_x86_64-linux/log/Refine.gz
the same for Bisim and Access.
Does this mean the size is 0 and probably nothing is written in this file? So there is no input and thus no output? If so can you please advice how to solve it?
Example:
:~/Desktop/verification/l4v$ ./isabelle/bin/isabelle build -d . -v -b Refine
Started at Tue Dec 20 11:44:16 EST 2016 (polyml-5.6_x86_64-linux on ssrgv-ThinkPad-T440p)
ISABELLE_BUILD_OPTIONS=""
ISABELLE_BUILD_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx2560m -Xss4m"
ML_PLATFORM="x86_64-linux"
ML_HOME="/home/ssrgv/.isabelle/contrib/polyml-5.6-1/x86_64-linux"
ML_SYSTEM="polyml-5.6"
ML_OPTIONS="-H 2000"
Session Pure/Pure
Session HOL/HOL (main)
Session HOL/HOL-Word (main)
Session Unsorted/Word_Lib
Session Specifications/ASpec
Session Proofs/AInvs
Session Proofs/BaseRefine
Session Proofs/Refine
*** I/O error
Finished at Tue Dec 20 11:44:19 EST 2016
0:00:03 elapsed time, 0:00:17 cpu time
—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub<#15>, or mute the thread<https://github.com/notifications/unsubscribe-auth/ANQQ8PeRHGRinBRoE39hr_eEMZyOBTsfks5rKAvUgaJpZM4LSElu>.
|
Thanks a lot Thomas! I was considering changing the names of the files i.e renaming the files, but your suggestion is more appropriate since their sizes were 0. Thus, I removed the files from the log then all three tests worked fine. However, one of the tests which was skipped previously " CRefine" -due to dependency -has failed. The message is below and a small question. I do appreciate your advise on how to fix it! Note: I had run this "CRefine" test independently before I managed to fix Refine test. So I removed it from the log file as well and then I retested it after the fix, but yet it gives the error 137: " Ignoring duplicate rewrite rule". The error message asks to see the log file -please see the full error message below. Thus, when I use zless CRefine, I can see the error "Ignoring duplicate rewrite rule" associated to some files such as: file=~/Desktop/verification/l4v/proof/crefine/Arch_C.thy^ Does this mean that I need to remove/rename crefine from proof directory as well- then retest? It seems like the proofs are corrupted maybe following the first independent building for CRefine? Or does the new sel4 modifications on CRfeine e.g on " Refine_c.thy" led to this? I have seen a comment for example on Refine_c.thy states that ; " New testfile for graph-refine export with new handling code. Also Again, I will appreciate your advise! Thanks in advance. Error 137: CRefine: theory Refine_C theory "Refine_C"53.794s elapsed time, 179.736s cpu time, 52.884s GC timeIgnoring duplicate rewrite rule:seL4_NonArchObjectTypeCount <equiv> 5Ignoring duplicate rewrite rule:ccorres_underlying ?sr1 ?<Gamma>1 ?r1 ?xf1 ?arrel1 ?axf1 ?P1 ?P'1 ?hs1(liftM ?t1 ?f1) ?g1 <equiv>ccorres_underlying ?sr1 ?<Gamma>1 (?r1 <circ> ?t1) ?xf1(?arrel1 <circ> ?t1) ?axf1 ?P1 ?P'1 ?hs1 ?f1 ?g1Bad Simplifier context: renamed bound variable ":001" to ":001a" (line 2786 of "~/Desktop/verification/l4v/proof/crefine/Retype_C.thy")Bad Simplifier context: renamed bound variable ":000" to ":000a" (line 2786 of "~/Desktop/verification/l4v/proof/crefine/Retype_C.thy")Bad Simplifier context: renamed bound variable ":000" to ":000a" (line 2786 of "~/Desktop/verification/l4v/proof/crefine/Retype_C.thy")Bad Simplifier context: renamed bound variable ":001" to ":001a" (line 2786 of "~/Desktop/verification/l4v/proof/crefine/Retype_C.thy")Bad Simplifier context: renamed bound variable ":000" to ":000a" (line 2786 of "~/Desktop/verification/l4v/proof/crefine/Retype_C.thy")Bad Simplifier context: renamed bound variable ":000" to ":000a" (line 2786 of "~/Desktop/verification/l4v/proof/crefine/Retype_C.thy")Bad Simplifier context: renamed bound variable ":000" to ":000a" (line 2786 of "~/Desktop/verification/l4v/proof/crefine/Retype_C.thy")Bad Simplifier context: renamed bound variable ":000" to ":000a" (line 2786 of "~/Desktop/verification/l4v/proof/crefine/Retype_C.thy")Bad Simplifier context: renamed bound variable ":001" to ":001a" (line 2786 of "~/Desktop/verification/l4v/proof/crefine/Retype_C.thy")Ignoring duplicate rewrite rule:objBits ?v <equiv> objBitsKO (injectKO ?v)Unfinished session(s): CRefine
|
Interesting, the log file seems to have only warnings, no errors, and it looks like the proof part actually finished successfully (theory "Refine_C"'/53.794s elapsed time, 179.736s cpu time, 52.884s GC time). It's possible that there was not enough RAM for polyml to prepare the image that is written to disk in the end. RAM requirements for CRefine are about 16GB currently, I think. Did the machine have that much available? |
Looking at our regression test, CRefine without constrained memory finishes with the following: CRefine passed ( 0:59:44 real, 3:10:32 cpu, 24.34GB) This means your run probably did not complete the proof (20:48min elapsed time from the log), but memory might indeed be the problem. The messages "Ignoring duplicate rewrite rule" and "Bad Simplifier context" are warnings and are expected output in the log file. Would you be able to attach the complete log file? |
Thanks a lot for your explanation! Yes, it seems like a memory issue! I checked the system information, the RAM falls short below 16 G. Its installed physical RAM is 16 G, but its total physical RAM is 15.9 G and the usable RAM is 15.6 G. It seems like a small part of the RAM is preserved to the hardware. To make sure that this lack of memory was the reason, I ran the system monitor application to observe the traffic while running the test. In deed, the point that the monitor reported ~15.6 G used with 99.7% usage of the RAM corresponded to the point it reached Refine_c in the log file. Then the machine became slow for a short while, then the warning message showed up and then the test stopped as can be seen in the attachments. For the full log please see the attachments: Thanks so much for the explanations! |
Hi All,
I am trying to run the Refine, Bisim, and Access tests in my new installation of Sel4 on a dual boot ubuntu 16.04-1 LTL (Xenial Xerus) . I did not get what the error message means, it is quite short (please see the example below). If someone can help I will appreciate that a lot.
One note: the first time I ran the tests on my dual boot machine the tests were interrupted due to the small Ubuntu partition size (~50 G at that time) the tests Refine, Bisim, and Acess all have been executing at that time and they failed due to lack of memory and nothing was written. Later I expanded the ubuntu partition (to 138 G), all tests- except these three-worked (some skipped due to dependencies). Moreover, when I
use:
" find $HOME -iname 'Refine.*' -size 0M " it returns :
/home/ssrgv/.isabelle/heaps-ARM-home-ssrgv-Desktop-verification-isabelle/polyml-5.6_x86_64-linux/log/Refine.gz
the same happens for Bisim and Access.
Does this mean the size is 0 and probably nothing is written in this file? So there is no input and thus no output? If so can you please advise how to solve it?
Example:
:~/Desktop/verification/l4v$ ./isabelle/bin/isabelle build -d . -v -b Refine
Started at Tue Dec 20 11:44:16 EST 2016 (polyml-5.6_x86_64-linux on ssrgv-ThinkPad-T440p)
ISABELLE_BUILD_OPTIONS=""
ISABELLE_BUILD_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx2560m -Xss4m"
ML_PLATFORM="x86_64-linux"
ML_HOME="/home/ssrgv/.isabelle/contrib/polyml-5.6-1/x86_64-linux"
ML_SYSTEM="polyml-5.6"
ML_OPTIONS="-H 2000"
Session Pure/Pure
Session HOL/HOL (main)
Session HOL/HOL-Word (main)
Session Unsorted/Word_Lib
Session Specifications/ASpec
Session Proofs/AInvs
Session Proofs/BaseRefine
Session Proofs/Refine
*** I/O error
Finished at Tue Dec 20 11:44:19 EST 2016
0:00:03 elapsed time, 0:00:17 cpu time
The text was updated successfully, but these errors were encountered: