<table cellspacing="0" cellpadding="0" border="0" ><tr><td valign="top" style="font: inherit;">Hi all:<br>I wonder how we could make the static M3CG stack allocation tracing verified so not overflow can occur and so make a progress with that compiler obligation too. <br>I suppose every thing we can put in the stack instead of the heap is less efficient in compiler and the checker times but in terms of execution less slower than it would without it.<br>I recall just an experiment with the ESC to check DISPOSE statement (side effecting) instruction will not corrupt the heap with the ESC, kind of interesting for the help M3CG to disable compiler inserted useless garbage collector calls and if so usable inside the stack boundaries for checking unused stack allocated callee for instance inside the bug commented by Mika on see:<br>https://mail.elegosoft.com/pipermail/m3devel/2010-December/008330.html<br>perhaps a mapping of the M3CG typed implementation
if we have already a reference to that unreachable code and if so will it be called or not according to the compiler code generator, in such a case there is a on-live dynamic linking it will just like it could prove it or not to not disable those callers, we would need to automatically infer the annotations for the checker to M3CG µ-instructions and feed for the checker and prover that too. This would be useful not just for the compiler, but for the programmer too, don't you think?<br>Also this would be straightforward to demonstrative of a program that is not to overflow or underflow by popping out anyhow, another missing check in current compilers technology as of what I currently know. Besides that one must check the arithmetic overflow, that would need more of the ESC normal technology by now, though we could explicitly check for it in the searched errors too, again typing the M3CG µ-instructions will gave some of the neeeded info I guess and by
emulating ALU logic we could also warn proof that anything would happen in some point if contracts are fulfilled.<br> <br>Thanks in advance <br><br>--- El <b>mié, 5/1/11, Jay K <i><jay.krell@cornell.edu></i></b> escribió:<br><blockquote style="border-left: 2px solid rgb(16, 16, 255); margin-left: 5px; padding-left: 5px;"><br>De: Jay K <jay.krell@cornell.edu><br>Asunto: Re: [M3commit] CVS Update: cm3<br>Para: "Tony" <hosking@cs.purdue.edu><br>CC: m3commit@elegosoft.com<br>Fecha: miércoles, 5 de enero, 2011 17:40<br><br><div id="yiv448101372">
<style><!--
#yiv448101372 .yiv448101372hmmessage P
{
margin:0px;padding:0px;}
#yiv448101372 .yiv448101372hmmessage
{
font-size:10pt;font-family:Tahoma;}
--></style>
I've back with full keyboard if more explanation needed. The diff is actually fairly small to read.<div>I understand it is definitely less efficient, a few more instructions for every try/lock.</div><div>No extra function call, at least with gcc backend.</div><div>I haven't tested NT386 yet. Odds are so/so that it works -- the change is written so that it should work</div><div>but I have to test it to be sure, will to roughly tonight. And there probably is a function call there.</div><div><br></div><div> - Jay<br><br><hr id="yiv448101372stopSpelling">From: jay.krell@cornell.edu<br>To: hosking@cs.purdue.edu<br>Date: Wed, 5 Jan 2011 20:44:08 +0000<br>CC: m3commit@elegosoft.com<br>Subject: Re: [M3commit] CVS Update: cm3<br><br>
<style>
#yiv448101372 .yiv448101372ExternalClass .yiv448101372ecxhmmessage P
{padding:0px;}
#yiv448101372 .yiv448101372ExternalClass body.yiv448101372ecxhmmessage
{font-size:10pt;font-family:Tahoma;}
</style>
I only have phone right now. I think it is fairly clear: the jumpbuf in EF1 is now allocated with alloca, and a pointer stored. It is definitely a bit less efficient, but the significant advantage is frontend no longer needs to know the size or alignment of a jumpbuf.<br><br><br>As well, there is no longer the problem regarding jumpbuf aligned to more than 64 bits. I at least checked on Linux/PowerPC and alloca seems to align to 16 bytes. I don't have an HPUX machine currently to see if the problem is addressed there.<br><br><br>The inefficiency of course can be dramatically mitigated via a stack walker. I wanted to do this first though, while more targets using setjmp.<br><br> - Jay/phone<br><br><hr>Subject: Re: [M3commit] CVS Update: cm3<br>From: hosking@cs.purdue.edu<br>Date: Wed, 5 Jan 2011 13:35:59 -0500<br>CC: jkrell@elego.de; m3commit@elegosoft.com<br>To: jay.krell@cornell.edu<br><br>
<base>Can you provide a more descriptive checkin comment? I don't know what has been done here without diving into the diff.<div><br><div><div>
<span class="yiv448101372ecxApple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px;"><span class="yiv448101372ecxApple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px;"><div style=""><span class="yiv448101372ecxApple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; text-indent: 0px; text-transform: none;
white-space: normal; word-spacing: 0px;"><span class="yiv448101372ecxApple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px;"><span class="yiv448101372ecxApple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px;"><span class="yiv448101372ecxApple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; text-indent:
0px; text-transform: none; white-space: normal; word-spacing: 0px;"><span class="yiv448101372ecxApple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px;"><span class="yiv448101372ecxApple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px;"><span class="yiv448101372ecxApple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal;
line-height: normal; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px;"><span class="yiv448101372ecxApple-style-span" style="border-collapse: separate; color: rgb(0, 0, 0); font-family: Helvetica; font-size: 12px; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px;"><div><font class="yiv448101372ecxApple-style-span" color="#0000ff"><font class="yiv448101372ecxApple-style-span" face="Gill Sans"><span class="yiv448101372ecxApple-style-span" style="color: rgb(0, 0, 255); font-family: 'Gill Sans';"><span class="yiv448101372ecxApple-style-span" style="color: rgb(0, 0, 255); font-family: 'Gill Sans';">Antony Hosking</span></span></font></font><font class="yiv448101372ecxApple-style-span" face="Gill Sans"><span class="yiv448101372ecxApple-style-span" style="font-family: 'Gill Sans';"><span
class="yiv448101372ecxApple-style-span" style="font-family: 'Gill Sans';"><span class="yiv448101372ecxApple-converted-space"> </span>|<span class="yiv448101372ecxApple-converted-space"> </span></span></span><span class="yiv448101372ecxApple-style-span" style="font-family: 'Gill Sans';"><span class="yiv448101372ecxApple-style-span" style="font-family: 'Gill Sans';">Associate Professor</span></span><span class="yiv448101372ecxApple-style-span" style="font-family: 'Gill Sans';"><span class="yiv448101372ecxApple-style-span" style="font-family: 'Gill Sans';"> | Computer Science | Purdue University</span></span></font></div><div><font class="yiv448101372ecxApple-style-span" face="GillSans-Light"><span class="yiv448101372ecxApple-style-span" style="font-family: GillSans-Light;">305 N. University Street | West Lafayette | IN 47907 | USA</span></font></div><div><font class="yiv448101372ecxApple-style-span" color="#0000ff" face="Gill Sans"><span
class="yiv448101372ecxApple-style-span" style="color: rgb(0, 0, 255); font-family: 'Gill Sans';"><span class="yiv448101372ecxApple-style-span" style="color: rgb(0, 0, 255); font-family: 'Gill Sans';">Office</span></span></font><font class="yiv448101372ecxApple-style-span" face="GillSans-Light"><span class="yiv448101372ecxApple-style-span" style="font-family: GillSans-Light;"><span class="yiv448101372ecxApple-style-span" style="font-family: GillSans-Light;"> +1 765 494 6001 |<span class="yiv448101372ecxApple-converted-space"> </span></span></span></font><font class="yiv448101372ecxApple-style-span" color="#0000ff" face="Gill Sans"><span class="yiv448101372ecxApple-style-span" style="color: rgb(0, 0, 255); font-family: 'Gill Sans';"><span class="yiv448101372ecxApple-style-span" style="color: rgb(0, 0, 255); font-family: 'Gill Sans';">Mobile</span></span></font><font class="yiv448101372ecxApple-style-span" face="GillSans-Light"><span
class="yiv448101372ecxApple-style-span" style="font-family: GillSans-Light;"><span class="yiv448101372ecxApple-style-span" style="font-family: GillSans-Light;"><span class="yiv448101372ecxApple-converted-space"> </span>+1 765 427 5484</span></span></font></div><div><font class="yiv448101372ecxApple-style-span" face="GillSans-Light"><br class="yiv448101372ecxkhtml-block-placeholder"></font></div></span></span></span></span></span></span></span><br class="yiv448101372ecxApple-interchange-newline"></span></div></span></span><br class="yiv448101372ecxApple-interchange-newline">
</div>
<br><div><div>On Jan 5, 2011, at 9:37 AM, Jay K wrote:</div><br class="yiv448101372ecxApple-interchange-newline"><blockquote><span class="yiv448101372ecxApple-style-span" style="border-collapse: separate; font-family: Helvetica; font-style: normal; font-variant: normal; font-weight: normal; letter-spacing: normal; line-height: normal; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; font-size: medium;"><div class="yiv448101372ecxhmmessage" style="font-size: 10pt; font-family: Tahoma;">diff attached<br><br>> Date: Wed, 5 Jan 2011 15:34:55 +0000<br>> To:<span class="yiv448101372ecxApple-converted-space"> </span><a rel="nofollow" ymailto="mailto:m3commit@elegosoft.com" target="_blank" href="/mc/compose?to=m3commit@elegosoft.com">m3commit@elegosoft.com</a><br>> From:<span class="yiv448101372ecxApple-converted-space"> </span><a rel="nofollow" ymailto="mailto:jkrell@elego.de" target="_blank"
href="/mc/compose?to=jkrell@elego.de">jkrell@elego.de</a><br>> Subject: [M3commit] CVS Update: cm3<br>><span class="yiv448101372ecxApple-converted-space"> </span><br>> CVSROOT: /usr/cvs<br>> Changes by: jkrell@birch. 11/01/05 15:34:55<br>><span class="yiv448101372ecxApple-converted-space"> </span><br>> Modified files:<br>> cm3/m3-libs/m3core/src/C/Common/: Csetjmp.i3<span class="yiv448101372ecxApple-converted-space"> </span><br>> cm3/m3-libs/m3core/src/C/I386_CYGWIN/: Csetjmp.i3<span class="yiv448101372ecxApple-converted-space"> </span><br>> cm3/m3-libs/m3core/src/C/I386_MINGW/: Csetjmp.i3<span class="yiv448101372ecxApple-converted-space"> </span><br>> cm3/m3-libs/m3core/src/C/I386_NT/: Csetjmp.i3<span class="yiv448101372ecxApple-converted-space"> </span><br>> cm3/m3-libs/m3core/src/C/NT386/: Csetjmp.i3<span class="yiv448101372ecxApple-converted-space"> </span><br>>
cm3/m3-libs/m3core/src/runtime/ex_frame/: RTExFrame.m3<span class="yiv448101372ecxApple-converted-space"> </span><br>> cm3/m3-libs/m3core/src/unix/Common/: Uconstants.c<span class="yiv448101372ecxApple-converted-space"> </span><br>> cm3/m3-sys/m3cc/gcc/gcc/m3cg/: parse.c<span class="yiv448101372ecxApple-converted-space"> </span><br>> cm3/m3-sys/m3front/src/misc/: Marker.m3<span class="yiv448101372ecxApple-converted-space"> </span><br>> cm3/m3-sys/m3front/src/stmts/: TryFinStmt.m3 TryStmt.m3<span class="yiv448101372ecxApple-converted-space"> </span><br>> cm3/m3-sys/m3middle/src/: M3RT.i3 M3RT.m3 Target.i3 Target.m3<span class="yiv448101372ecxApple-converted-space"> </span><br>><span class="yiv448101372ecxApple-converted-space"> </span><br>> Log message:<br>> use: extern INTEGER Csetjmp__Jumpbuf_size /* = sizeof(jmp_buf);<br>> alloca(Csetjmp__Jumpbuf_size)<br>><span
class="yiv448101372ecxApple-converted-space"> </span><br>> to allocate jmp_buf<br>><span class="yiv448101372ecxApple-converted-space"> </span><br>> - eliminates a large swath of target-dependent code<br>> - allows for covering up the inability to declare<br>> types with alignment > 64 bits<br>><span class="yiv448101372ecxApple-converted-space"> </span><br>> It is, granted, a little bit slower, in an already prety slow path.<br>> Note that alloca isn't actually a function call, at least with gcc backend.<br>><span class="yiv448101372ecxApple-converted-space"> </span><br><span><jmpbuf_alloca.txt></span></div></span></blockquote></div><br></div></div></div>
</div></blockquote></td></tr></table><br>