Traces – less ordered strings (part 1)

I decided to read about Traces. I’m going to tell you I learnt to try and cement the ideas in my mind.

First off, strings have two more monoid natures! It is on the removal of the first occurrence of string a from string b from the left or right. Both the monoid natures have the empty string as the mempty.

So remR "cabcabac" "ab" would be “cabcac” whereas remL "cabcabac" "ab" would be “ccabac”. Removal of a string that isn’t contained leads to no change. This is called the quotient monoid I think, I still don’t have the terminology down.

Traces are strings when you don’t care about some ordering in them. Something like the following untested bit of code

class (ListLike a, Enum a, Bounded a, Eq a) =>Trace a where
   swappablePairs :: Set (a,a)
   swappablePairs = difference (cross [minBound..maxBound] [minBound..maxBound])  unswappablePairs
   unswappablePairs :: Set (a,a)
   unswappablePairs = difference (cross [minBound..maxBound] [minBound..maxBound])  swappablePairs
   traceEq :: Trace a  -> Trace a -> Bool

Note when I say (a,c) is swappable I also mean (c,a) is swappable.

So an example of a trace applied somewhat to seeing what a processor is doing. Lets say we have two cores that share a bit of memory they are working on. The symbols a and b represent each process acting on the shared memory, also (a,b) and (b,a) is swappable. So let us define another pair of operations that represent the cores handing off to each other c is core 1 handing to core 2 and d is core 2 to core 1. So (a,c) is unswappable as you can’t move operations before or after blocking and so is (b,d). (c,d) is also unswappable. e is nothing interesting going on and is swapabble with anything.

So a trace “aeeeeb” should be traceEq to “eeeeab” that is both cores writing to shared memory with no hand off, which is bad. “aaeeceeebbbeeda” is traceEq to “eeeeeacbda”, which is fine as there are the proper hand offs between ‘a’s and ‘b’s. This doesn’t seem so useful at the moment, although I think things get more interesting when you have two different bits of shared memory that can interleave.

The way I’m guessing it is used in process calculi is that you generate grammars for the processes and then see if the space of all possible strings on the language contains sequences traceEq to things you don’t want e.g. a and b next door to each others or an infinite sequence of hand offs with no processing. Quite how to do that I am unsure….

Are they useful for what I want to do? Possibly, I think I will give people the option of specifying a writer or something similar to go a long and build up traces or something, by processing the current Vrrm state and assigning it a symbol. Ideally there should be some way of discovering the grammar as well… though I am not sure how to do this, although it might be easy(ish) if the symbol assignment process doesn’t hide state.

Next time I’ll try to implement instances of traceEq, and make sure my implementation of Trace is actually sane.

Advertisement