<html>
<head>
<style><!--
.hmmessage P
{
margin:0px;
padding:0px
}
body.hmmessage
{
font-size: 10pt;
font-family:Tahoma
}
--></style>
</head>
<body class='hmmessage'>
The gcc compiler is already optimizing.<br>The integrated backend always optimizes a bit and produces half decent code. Fairly local optimizations though, very very very simple analysis.<br>I'd like the machines to be powered off when idle, not find more ways to keep them busy.<br><br><br>As well, most of the analysis is "portable" -- only needs to be one for one target, not all, so unless it is really large and easily distributed, just one machine.<br><br><br>If we really are interested static analysis, a C or C++ or heck C# or Java generating backend plus throwing their static analyzers around is the way to go.<br> There is far more energy thrown at other languages, and actually significant results, despite the starting point.<br> Some tools might analyze binaries. valgrind?<br><br>Modula-3 and ESC were ahead of their time at some point, but the world has largely caught up and in many ways surpassed.<br>For example, Modula-3 was perhaps perhaps better than DCOM and CORBA, but these days, connected remoting has been deemed non-scalable and disconnected remoting is largely used, esp. via http.<br><br><br> - Jay<br><br><br>> Date: Thu, 6 Jan 2011 13:28:18 +0000<br>> From: dabenavidesd@yahoo.es<br>> To: wagner@elegosoft.com<br>> CC: m3devel@elegosoft.com<br>> Subject: Re: [M3devel] elegosoft.com working?<br>> <br>> Hi all:<br>> yes, but maybe when if we got around an optimizing compiler we would need the verification condition generator to use the theorem prover, so the same deal again, and if so we would need also build machines dedicated also to that, I mean what is the point of having them to keeping idle while something in contrast would highly optimized it instead. I bet even the compiler is also to have optimization by it self, I guess everything would need to and so the optimization framework would need to run the theorem prover to work in each build. Even the Simplify, so we must keep and eye on it too meanwhile.<br>> <br>> Thanks in advance <br>> <br>> --- El jue, 6/1/11, Olaf Wagner <wagner@elegosoft.com> escribió:<br>> <br>> > De: Olaf Wagner <wagner@elegosoft.com><br>> > Asunto: Re: [M3devel] elegosoft.com working?<br>> > Para: "Daniel Alejandro Benavides D." <dabenavidesd@yahoo.es><br>> > CC: m3devel@elegosoft.com<br>> > Fecha: jueves, 6 de enero, 2011 06:56<br>> > Let's worry about ESC integration<br>> > when we get access to it.<br>> > Anyway, I wouldn't run such checks in every build, but<br>> > perform it<br>> > on a certain machine e.g. once a day.<br>> > <br>> > Olaf<br>> > <br>> > Quoting "Daniel Alejandro Benavides D." <dabenavidesd@yahoo.es>:<br>> > <br>> > > Hi all:<br>> > > I recall now that the current rend is run this theorem<br>> > provers distributedly, rather than standalone, so we<br>> > might given that we have already this in our hands the<br>> > Simplify theorem prover, for a network instance, not<br>> > sure if the I/O will be affected in that case, perhaps<br>> > the most important thing is to verify full integrity<br>> > of transfers. See about that issue:<br>> > > http://nexus.realtimepublishers.com/ttgmft.php<br>> > > (is a work in progress so if interested keep and eye<br>> > on it, you can register if you want)<br>> > > Given that simplify is not written object oriented,<br>> > perhaps that must be thought to be like that. The<br>> > thing is given it takes more than double times the<br>> > time of the compile build process we might (the Greg<br>> > nelson comment at 53:00 on the linked video) is it is<br>> > a kind of slow process or of high length but ok to be<br>> > run on nights. Perhaps given that the compiler<br>> > building could take 2x a compiler build and the<br>> > theorem proving 5x times that, which is we can run it <br>> > each 5 runs in terms of the of two builds, i.e m3tk<br>> > included. The thing is, if the source has not changed<br>> > that is would be the case in some runs it could be in<br>> > terms of less runs, so we can check in at least each 5<br>> > building tasks runs (of all platforms, i.e 5 parallel <br>> > building tasks), I guess this tasks are programmed in some<br>> > way, I don't recall where are the policies of this<br>> > written, if someone can tell that for me or point me<br>> > that, thanks in advance<br>> > > <br>> > > <br>> > > --- El mié, 5/1/11, Daniel Alejandro Benavides<br>> > D. <dabenavidesd@yahoo.es><br>> > escribió:<br>> > > <br>> > >> De: Daniel Alejandro Benavides D. <dabenavidesd@yahoo.es><br>> > >> Asunto: Re: [M3devel] elegosoft.com working?<br>> > >> Para: "Olaf Wagner" <wagner@elegosoft.com><br>> > >> CC: m3devel@elegosoft.com<br>> > >> Fecha: miércoles, 5 de enero, 2011 11:28<br>> > >> Hi all:<br>> > >> yes, I think we should get access to building with<br>> > cm3 at<br>> > >> least, not sure if the sources according to the<br>> > latest news<br>> > >> on that.<br>> > >> In the other hand whether we get this I hope<br>> > sooner or<br>> > >> later, I think it would be a m3quake directive<br>> > like "esc()"<br>> > >> to activate it from inside the building task<br>> > process, so it<br>> > >> can be integrated on the same building machine or<br>> > another<br>> > >> will need to have access to the same CM3 build and<br>> > source<br>> > >> repository and check it on the way, the only thing<br>> > here, is<br>> > >> that ESC need to build M3 sources with m3tk and if<br>> > so, it<br>> > >> will that aprox. by the same time cm3 compiler<br>> > building<br>> > >> software ends that ESC will feed itself with cm3<br>> > M3Build<br>> > >> .M3IMPTAB import table not generated file now<br>> > times for<br>> > >> external compilers. I'm not sure anyway if that's<br>> > the order<br>> > >> of ESC input anyway, or will need first the<br>> > .M3IMPPTAB back<br>> > >> again perhaps will need to upgrade down or make a<br>> > better<br>> > >> independent procedure to expose this for it, see<br>> > Revision<br>> > >> 1.24:<br>> > >> http://dcvs.elegosoft.com/cgi-bin/cvsweb.cgi/cm3/m3-sys/cm3/src/M3Build.m3?annotate=1.24<br>> > >> if that's the case we would need to wait anyway<br>> > for cm3<br>> > >> builds or call it from the IMPORTS to get it.<br>> > Please if one<br>> > >> can check that if it's need it and I will likely<br>> > to see that<br>> > >> too. I also think this would be a nice way of<br>> > making a<br>> > >> dependence analyzer (if so perhaps I think is<br>> > better doing<br>> > >> it with m3tk, what do you think? Besides its worth<br>> > for Obliq<br>> > >> and others too like cm3ide, etc) program for<br>> > our and<br>> > >> other clients too information IMHO.<br>> > >> Thanks in advance<br>> > >> <br>> > >> P.D: according to Dr Greg Nelson the compiler is<br>> > usually<br>> > >> 10x times faster than the ESC process (not sure<br>> > for the<br>> > >> ESC/Java or the ESC/Moddula3), but this is mostly<br>> > because of<br>> > >> the Simplify theorem prover checking see:<br>> > >> http://www.uwtv.org/programs/displayevent.aspx?rID=2761<br>> > >> Also for simplify see:<br>> > >> http://portal.acm.org/citation.cfm?id=1066100.1066102&preflayout=flat<br>> > >> whican can be downlaoded report from here:<br>> > >> http://www.hpl.hp.com/techreports/2003/HPL-2003-148.html<br>> > >> and benchmarks from here:<br>> > >> http://goedel.cs.uiowa.edu/smtlib/benchmarks/pending/simplify_benchmarks.tar.gz<br>> > >> <br>> > >> <br>> > >> --- El mié, 5/1/11, Olaf Wagner <wagner@elegosoft.com><br>> > >> escribió:<br>> > >> <br>> > >> > De: Olaf Wagner <wagner@elegosoft.com><br>> > >> > Asunto: Re: [M3devel] elegosoft.com working?<br>> > >> > Para: "Daniel Alejandro Benavides D." <dabenavidesd@yahoo.es><br>> > >> > CC: m3devel@elegosoft.com<br>> > >> > Fecha: miércoles, 5 de enero, 2011 04:04<br>> > >> > Quoting "Daniel Alejandro Benavides<br>> > >> > D." <dabenavidesd@yahoo.es>:<br>> > >> ><br>> > >> > > Hi all:<br>> > >> > > thanks for the info, some time after it<br>> > went on<br>> > >> again<br>> > >> > working, but still if there is some<br>> > escalation<br>> > >> issue<br>> > >> > because of the compiler checks<br>> > specially with<br>> > >> the<br>> > >> > computation time, like ESC and so,<br>> > perhaps like<br>> > >> in<br>> > >> > night builds, what would be the machine needs<br>> > for that<br>> > >> <br>> > >> > process and the results to allow?<br>> > >> > > Based on some experience like in<br>> > compilers we<br>> > >> would<br>> > >> > have access to the checks in more or<br>> > less time<br>> > >> if so I<br>> > >> > guess we would need optimization anyway<br>> > at<br>> > >> source<br>> > >> > level and execution level. Meanwhile <br>> > more checks<br>> > >> will<br>> > >> > likely to be introduced, so it would a<br>> > balance<br>> > >> of both<br>> > >> > needs.<br>> > >> > > Thanks in advance<br>> > >> ><br>> > >> > I'm not sure if I understand correctly what<br>> > you're<br>> > >> aiming<br>> > >> > at, but<br>> > >> > I guess you worry that we need to introduce<br>> > more<br>> > >> > checks/tests like<br>> > >> > ESC. Apart from my estimation that we won't<br>> > get access<br>> > >> to<br>> > >> > the ESC M3<br>> > >> > sources, CPU time would not be a bottleneck,<br>> > as (a)<br>> > >> the<br>> > >> > bottleneck on<br>> > >> > birch is the I/O system and (b) we could<br>> > easily<br>> > >> delegate<br>> > >> > such a task<br>> > >> > to another server via Hudson. Anyway, once<br>> > the web<br>> > >> service<br>> > >> > has been<br>> > >> > moved to another machine there shouldn't be<br>> > any more<br>> > >> > problems with<br>> > >> > our use of birch.<br>> > >> ><br>> > >> > Olaf<br>> > >> > --Olaf Wagner -- elego Software Solutions<br>> > GmbH<br>> > >> ><br>> > >> > Gustav-Meyer-Allee 25 / Gebäude<br>> > 12,<br>> > >> 13355<br>> > >> > Berlin, Germany<br>> > >> > phone: +49 30 23 45 86 96 mobile: +49<br>> > 177 2345<br>> > >> > 869 fax: +49 30 23 45 86 95<br>> > >> > http://www.elegosoft.com |<br>> > >> > Geschäftsführer: Olaf Wagner | Sitz:<br>> > Berlin<br>> > >> > Handelregister: Amtsgericht Charlottenburg<br>> > HRB 77719<br>> > >> |<br>> > >> > USt-IdNr: DE163214194<br>> > >> ><br>> > >> ><br>> > >> <br>> > >> <br>> > >> <br>> > >> <br>> > > <br>> > > <br>> > > <br>> > > <br>> > <br>> > <br>> > <br>> > --Olaf Wagner -- elego Software Solutions GmbH<br>> > <br>> > Gustav-Meyer-Allee 25 / Gebäude 12, 13355<br>> > Berlin, Germany<br>> > phone: +49 30 23 45 86 96 mobile: +49 177 2345<br>> > 869 fax: +49 30 23 45 86 95<br>> > http://www.elegosoft.com |<br>> > Geschäftsführer: Olaf Wagner | Sitz: Berlin<br>> > Handelregister: Amtsgericht Charlottenburg HRB 77719 |<br>> > USt-IdNr: DE163214194<br>> > <br>> > <br>> <br>> <br>> <br> </body>
</html>