[M3devel] elegosoft.com working?

Thu Jan 6 23:04:43 CET 2011

Hi all:
yes, I think the current is to run the testing distributed, rather than standalone, this is because of memory and essentially because it aims to be like that distributed rather than standalone runs in those cases we have that scenario, perhaps the one most feasible if so, because inside the prover there is a logic programming language, so the idea  of writing solvers in Java, etc, is not bad, anyway there is a interpreter in it, but we have a good tool already, a good language and seeing it more now it seems to be object oriented at some of it (I have now a compiler error <*NOWARN*> used to avoid somehow before when compiling the prover library), I read they were a compact team of developers but same comments I have read about Modula-3 not being so much object oriented restrictive language, and they have a reason language is not just object oriented I think, if we needed it to run distributed, we would likely to do it with and automatic parallelization,
 with a Compiler Static Analyzer to produce a concurrent server, see: http://www.usenix.org/publications/library/proceedings/sedms4/sims.html
then I guess we could think how to distribute that, which guarantees the semantics of the system won't be touched, then if we just write in terms of another checker, like an ESC/Obliq, the semantics will be not touched and be happy about type checks because it has type inference or reconstruction so that guarantees that the type checking would be not needed and it will just have in terms of checks the simplify process as normal but also of a more object oriented fashion which is what the others are aiming to optimization, specially in C# and Java solvers. Perhaps that's the way to go, I guess the basics we could mimic and the internal structure put in Core Libraries of Modula-3 we would have safe distributed checking inside the Language itself and the better approach with this would be to solve first a test of the system performance: there was an experiment of the constraint solver procedure inside the Juno-2, done by Greg Nelson, during development of
 the project, they needed to make sure they would have scalable constraint resolution in large programs to be able to be doable in those, so did an experiment with it in the project Juno development, it however didn't prove too much but because of its continuous development but did make realize the system 
http://modula3.elegosoft.com/cm3/doc/help/gen_html/juno-machine/src/JunoByteCode.i3.html
was performing some how, due changes because they need to proof the real performance for the sessions interactivity they need to render in the screen while doing the Juno modifications, they would needed the binaries size so made information useless. It is suggested that a log with a symbol table would allow the logs to be useful even if modifications happened, by storing the binaries if necessary. In ESC/Obliq and Simplify, Obliq  hypothetic development case just an amount of effort to check the prover scalability will be needed given the uneeded binary information, although further improvement would allow a JIT for core parts I guess. see:
see: ftp://gatekeeper.pa.dec.com/pub/DEC/SRC/research-reports/SRC-153.pdf
(I realize late the relation between juno-machine and the Obliq interpreter)
Other approaches than those I guess would like to see the within the tool in compile time manner, that's why I think in a more fashionable yet correct form of doing ESC looking for that opportunity would in that safe manners help us.
Thanks in advance

--- El jue, 6/1/11, Jay K <jay.krell at cornell.edu> escribió:

De: Jay K <jay.krell at cornell.edu>
Asunto: RE: [M3devel] elegosoft.com working?
Para: dabenavidesd at yahoo.es, "Olaf" <wagner at elegosoft.com>
CC: "m3devel" <m3devel at elegosoft.com>
Fecha: jueves, 6 de enero, 2011 10:56

The gcc compiler is already optimizing.
The integrated backend always optimizes a bit and produces half decent code. Fairly local optimizations though, very very very simple analysis.
I'd like the machines to be powered off when idle, not find more ways to keep them busy.

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.

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.
  There is far more energy thrown at other languages, and actually significant results, despite the starting point.
  Some tools might analyze binaries. valgrind?

Modula-3 and ESC were ahead of their time at some point, but the world has largely caught up and in many ways surpassed.
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.

 - Jay

> Date: Thu, 6 Jan 2011 13:28:18 +0000
> From: dabenavidesd at yahoo.es
> To: wagner at elegosoft.com
> CC: m3devel at elegosoft.com
> Subject: Re: [M3devel] elegosoft.com working?
> 
> Hi all:
> 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.
>  
> Thanks in advance  
> 
> --- El jue, 6/1/11, Olaf Wagner <wagner at elegosoft.com> escribió:
> 
> > De: Olaf Wagner <wagner at elegosoft.com>
> > Asunto: Re: [M3devel] elegosoft.com working?
> > Para: "Daniel Alejandro Benavides D." <dabenavidesd at yahoo.es>
> > CC: m3devel at elegosoft.com
> > Fecha: jueves, 6 de enero, 2011 06:56
> > Let's worry about ESC integration
> > when we get access to it.
> > Anyway, I wouldn't run such checks in every build, but
> > perform it
> > on a certain machine e.g. once a day.
> > 
> > Olaf
> > 
> > Quoting "Daniel Alejandro Benavides D." <dabenavidesd at yahoo.es>:
> > 
> > > Hi all:
> > > I recall now that the current rend is run this theorem
> > provers  distributedly, rather than standalone, so we
> > might given that we  have already this in our hands the
> > Simplify theorem prover, for a  network instance, not
> > sure if the I/O will be affected in that case,  perhaps
> > the most important thing is to verify full integrity
> > of  transfers. See about that issue:
> > > http://nexus.realtimepublishers.com/ttgmft.php
> > > (is a work in progress so if interested keep and eye
> > on it, you can  register if you want)
> > > Given that simplify is not written object oriented,
> > perhaps that  must be thought to be like that. The
> > thing is given it takes more  than double times the
> > time of the compile build process we might  (the Greg
> > nelson comment at 53:00 on the linked video) is it is
> > a  kind of slow process or of high length but ok to be
> > run on nights.  Perhaps given that the compiler
> > building could take 2x a compiler  build and the
> > theorem proving 5x times that, which is we can run it 
> > each 5 runs in terms of the of two builds, i.e m3tk
> > included. The  thing is, if the source has not changed
> > that is would be the case in  some runs it could be in
> > terms of less runs, so we can check in at  least each 5
> > building tasks runs (of all platforms, i.e 5 parallel 
> > building tasks), I guess this tasks are programmed in some
> > way, I  don't recall where are the policies of this
> > written, if someone can  tell that for me or point me
> > that, thanks in advance
> > > 
> > > 
> > > --- El mié, 5/1/11, Daniel Alejandro Benavides
> > D.  <dabenavidesd at yahoo.es>
> > escribió:
> > > 
> > >> De: Daniel Alejandro Benavides D. <dabenavidesd at yahoo.es>
> > >> Asunto: Re: [M3devel] elegosoft.com working?
> > >> Para: "Olaf Wagner" <wagner at elegosoft.com>
> > >> CC: m3devel at elegosoft.com
> > >> Fecha: miércoles, 5 de enero, 2011 11:28
> > >> Hi all:
> > >> yes, I think we should get access to building with
> > cm3 at
> > >> least, not sure if the sources according to the
> > latest news
> > >> on that.
> > >> In the other hand whether we get this I hope
> > sooner or
> > >> later, I think it would be a m3quake directive
> > like "esc()"
> > >> to activate it from inside the building task
> > process, so it
> > >> can be integrated on the same building machine or
> > another
> > >> will need to have access to the same CM3 build and
> > source
> > >> repository and check it on the way, the only thing
> > here, is
> > >> that ESC need to build M3 sources with m3tk and if
> > so, it
> > >> will that aprox. by the same time cm3 compiler
> > building
> > >> software ends that ESC will feed itself with cm3
> > M3Build
> > >> .M3IMPTAB import table not generated file now
> > times for
> > >> external compilers. I'm not sure anyway if that's
> > the order
> > >> of ESC input anyway, or will need first the
> > .M3IMPPTAB back
> > >> again perhaps will need to upgrade down or make a
> > better
> > >> independent procedure to expose this for it, see
> > Revision
> > >> 1.24:
> > >> http://dcvs.elegosoft.com/cgi-bin/cvsweb.cgi/cm3/m3-sys/cm3/src/M3Build.m3?annotate=1.24
> > >> if that's the case we would need to wait anyway
> > for cm3
> > >> builds or call it from the IMPORTS to get it.
> > Please if one
> > >> can check that if it's need it and I will likely
> > to see that
> > >> too. I also think this would be a nice way of
> > making a
> > >> dependence analyzer (if so perhaps I think is
> > better doing
> > >> it with m3tk, what do you think? Besides its worth
> > for Obliq
> > >> and others too like cm3ide, etc)  program for
> > our and
> > >> other clients too information IMHO.
> > >> Thanks in advance
> > >> 
> > >> P.D: according to Dr Greg Nelson the compiler is
> > usually
> > >> 10x times faster than the ESC process (not sure
> > for the
> > >> ESC/Java or the ESC/Moddula3), but this is mostly
> > because of
> > >> the Simplify theorem prover checking see:
> > >> http://www.uwtv.org/programs/displayevent.aspx?rID=2761
> > >> Also for simplify see:
> > >> http://portal.acm.org/citation.cfm?id=1066100.1066102&preflayout=flat
> > >> whican can be downlaoded report from here:
> > >> http://www.hpl.hp.com/techreports/2003/HPL-2003-148.html
> > >> and benchmarks from here:
> > >> http://goedel.cs.uiowa.edu/smtlib/benchmarks/pending/simplify_benchmarks.tar.gz
> > >> 
> > >> 
> > >> --- El mié, 5/1/11, Olaf Wagner <wagner at elegosoft.com>
> > >> escribió:
> > >> 
> > >> > De: Olaf Wagner <wagner at elegosoft.com>
> > >> > Asunto: Re: [M3devel] elegosoft.com working?
> > >> > Para: "Daniel Alejandro Benavides D." <dabenavidesd at yahoo.es>
> > >> > CC: m3devel at elegosoft.com
> > >> > Fecha: miércoles, 5 de enero, 2011 04:04
> > >> > Quoting "Daniel Alejandro Benavides
> > >> > D." <dabenavidesd at yahoo.es>:
> > >> >
> > >> > > Hi all:
> > >> > > thanks for the info, some time after it
> > went on
> > >> again
> > >> > working, but  still if there is some
> > escalation
> > >> issue
> > >> > because of the compiler  checks
> > specially with
> > >> the
> > >> > computation time, like ESC and so,
> > perhaps  like
> > >> in
> > >> > night builds, what would be the machine needs
> > for that
> > >> 
> > >> > process and the results to allow?
> > >> > > Based on some experience like in
> > compilers we
> > >> would
> > >> > have access to  the checks in more or
> > less time
> > >> if so I
> > >> > guess we would need  optimization anyway
> > at
> > >> source
> > >> > level and execution level. Meanwhile 
> > more checks
> > >> will
> > >> > likely to be introduced, so it would a
> > balance
> > >> of  both
> > >> > needs.
> > >> > > Thanks in advance
> > >> >
> > >> > I'm not sure if I understand correctly what
> > you're
> > >> aiming
> > >> > at, but
> > >> > I guess you worry that we need to introduce
> > more
> > >> > checks/tests like
> > >> > ESC. Apart from my estimation that we won't
> > get access
> > >> to
> > >> > the ESC M3
> > >> > sources, CPU time would not be a bottleneck,
> > as (a)
> > >> the
> > >> > bottleneck on
> > >> > birch is the I/O system and (b) we could
> > easily
> > >> delegate
> > >> > such a task
> > >> > to another server via Hudson. Anyway, once
> > the web
> > >> service
> > >> > has been
> > >> > moved to another machine there shouldn't be
> > any more
> > >> > problems with
> > >> > our use of birch.
> > >> >
> > >> > Olaf
> > >> > --Olaf Wagner -- elego Software Solutions
> > GmbH
> > >> >
> > >> >    Gustav-Meyer-Allee 25 / Gebäude
> > 12,
> > >> 13355
> > >> > Berlin, Germany
> > >> > phone: +49 30 23 45 86 96  mobile: +49
> > 177 2345
> > >> > 869  fax: +49 30 23 45 86 95
> > >> >    http://www.elegosoft.com |
> > >> > Geschäftsführer: Olaf Wagner | Sitz:
> > Berlin
> > >> > Handelregister: Amtsgericht Charlottenburg
> > HRB 77719
> > >> |
> > >> > USt-IdNr: DE163214194
> > >> >
> > >> >
> > >> 
> > >> 
> > >> 
> > >> 
> > > 
> > > 
> > > 
> > > 
> > 
> > 
> > 
> > --Olaf Wagner -- elego Software Solutions GmbH
> >            
> >    Gustav-Meyer-Allee 25 / Gebäude 12, 13355
> > Berlin, Germany
> > phone: +49 30 23 45 86 96  mobile: +49 177 2345
> > 869  fax: +49 30 23 45 86 95
> >    http://www.elegosoft.com |
> > Geschäftsführer: Olaf Wagner | Sitz: Berlin
> > Handelregister: Amtsgericht Charlottenburg HRB 77719 |
> > USt-IdNr: DE163214194
> > 
> > 
> 
> 
>       

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://m3lists.elegosoft.com/pipermail/m3devel/attachments/20110106/452fffb7/attachment-0002.html>