Thank you for your answer, Robby. Actually at the beginning I planned to implement another version of the semantics in Coq and prove something useful about it. But before spending (a lot of) time with Coq version, it's better to be sure that the semantics is something I want, as you mentioned. And for this purpose I need to be able to run tests, which are little bit bigger than ones I can run in a reasonable time now. So I still wonder if there are some guidelines, which can help me with my current Redex version.
My supervisor suggested to implement the semantics in Racket, w/o using Redex reduction engine, but reusing some Redex functionality (e.g. `traces` and `stepper` functions, which are extremely useful). Is it a good idea? BR, Anton Podkopaev 2015-12-03 19:44 GMT+03:00 Robby Findler <ro...@eecs.northwestern.edu>: > Redex isn't really designed with performance in mind. Some future > version of Redex will probably improve on this, but perhaps not enough > for the use case you have in mind. > > My best advice (which is kind of depressing that this is the best I > can do) is to experiment with the Redex version until you're pretty > sure that you have something you like and then to implement another > version of the language in some inherently more efficient way. Then > you can use the Redex version to experiment with variations and to > provide a test oracle for the more efficient implementation. > > hth, > Robby > > > On Thu, Dec 3, 2015 at 10:14 AM, Anton Podkopaev <podkoav...@gmail.com> > wrote: > > Hello, dear colleagues! > > Could you, please, answer some of my questions? > > > > 1) Is there any paper about how the Racket engine works? > > 2) Is there any guide or a paper about effective (in terms of semantics > execution) Redex usage? > > > > I want to know it because I'm interested in optimizing my semantics in > Redex. > > > > What I want to find in aforementioned papers: > > - Are environments and holes effective, or I should use them rarely? > > - Is there any factorization of states during the reduction process? > > - ... > > > > Background story: > > I'm working on highly non-deterministic semantics for a concurrent > language using PLT/Redex. Unfortunately, I faced a performance problem --- > an execution of some tests, which aren't so big, takes too much time (> 40 > minutes). Originally, I though that the problem was in my heap > representation and I should have factorized it. But an execution of a > smaller test w/ only 280 states according to `traces` and w/o any > heap-related problems takes 30 seconds, which is still too much in my > opinion. > > > > --- > > Best regards, > > Anton Podkopaev, PhD student, SPbSU > > > > -- > > You received this message because you are subscribed to the Google > Groups "Racket Users" group. > > To unsubscribe from this group and stop receiving emails from it, send > an email to racket-users+unsubscr...@googlegroups.com. > > For more options, visit https://groups.google.com/d/optout. > -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
