It looks like your semantics has a lot of different ways to reach the same term (ie the reduction graph has a lot of sharing in it).
In it's default mode, test-->> (and apply-reduction-relation*) will not notice this sharing and explore all of the different paths, which can be very expensive. I think you want to do this: (current-cache-all? #t) That should speed up the test case for (term (,term_Big defaultState)) by about 50x and perhaps you will see similar speedups on other test cases. There is a little more discussion in the docs for apply-reduction-relation*. Robby On Fri, Dec 4, 2015 at 9:32 AM, Anton Podkopaev <podkoav...@gmail.com> wrote: >> One thing to check for is ambiguous patterns. Those can cause >> exponential blowup internally in Redex. > > Yes, there are a lot of ambiguous patterns, but it's made intentionally. > Most of the rules have such structure: > (--> ((in-hole E operation) globalState) > ((in-hole E (ret value)) globalState')) > where > [E hole > (E >>= K) > (par E Expr) > (par Expr E)] > and the `par` constructor is used to represent different threads. > > The performance problem is actual for terms with four threads of such > structure, even if `expr`* are small ones: > (par (par expr0 > expr1) > (par expr2 > expr3)) > >> But just to double check: when you run one of the examples that takes >> a long time, how many different terms are you getting? Millions or >> dozens? If dozens, then we may have a hope of fixing something. > > I think there are thousands of terms. As I mentioned before I'm not > completely satisfied with performance even for cases with 270 terms. > BTW, is there a better way to get a number of terms than to execute > `traces` and see a number it shows? > >> As for implementing it in Racket, if you write the one-step function >> of a reduction semantics as a Racket function, then you can certainly >> use traces to visualize it. One trick is to write: > > Thank you, it's realy nice trick. > >> If you have a concrete example that you think is mysteriously slow, >> then perhaps you could send me a complete program (that runs that >> example)? I would be happy to take a look. > > Yes, I have some examples, but they are too complex to be shown, > and it'll take too much time to extract them from the project, but they are > here: > - `term_Big` is a term, a reduction of which leads to 270 terms according > to `traces`, and `test-->>` run takes 30 seconds. I think it should be > much faster. > - The `test-->>` run for `term_WW_WRMW_W_RRR` takes dozens of minutes. > Appropriate `test-->>` calls are commented out. > > The project: https://github.com/anlun/OperationalSemanticsC11 > The file with terms: > https://github.com/anlun/OperationalSemanticsC11/blob/master/test%2FrelAcqNaRlxPost_t1.rkt > > > BR, > Anton Podkopaev > > 2015-12-04 15:52 GMT+03:00 Robby Findler <ro...@eecs.northwestern.edu>: >> >> Well, maybe there is a bug somewhere; if you're trying to run >> paper-sized examples you should be able to get them to complete >> reasonably quickly. >> >> One thing to check for is ambiguous patterns. Those can cause >> exponential blowup internally in Redex. >> >> But just to double check: when you run one of the examples that takes >> a long time, how many different terms are you getting? Millions or >> dozens? If dozens, then we may have a hope of fixing something. >> >> As for implementing it in Racket, if you write the one-step function >> of a reduction semantics as a Racket function, then you can certainly >> use traces to visualize it. One trick is to write: >> >> (define-language empty) >> (reduction-relation empty (--> any ,(call-my-racket-implementation >> (term any)))) >> >> I would say that if you do do that and the time to reduce goes from 40 >> minutes to milliseconds, then there is either a performance bug in >> Redex or an ambiguity that's tripping Redex up in the patterns in your >> language (or they are not the same language, I suppose). >> >> If you have a concrete example that you think is mysteriously slow, >> then perhaps you could send me a complete program (that runs that >> example)? I would be happy to take a look. >> >> Robby >> >> >> On Fri, Dec 4, 2015 at 5:14 AM, Anton Podkopaev <podkoav...@gmail.com> >> wrote: >> > 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. > > -- 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.
