DistCompiler / pgo

PGo is a source to source compiler from Modular PlusCal specs into Go programs.
https://distcompiler.github.io/
Apache License 2.0
173 stars 13 forks source link

Tracing gui using ShiViz #231

Open gedw99 opened 2 years ago

gedw99 commented 2 years ago

Am new here .

Really nice framework .

ShiViz is working with this code base, so that I can see the evacuation history ?

bestchai commented 2 years ago

Hi Gerard,

Thanks for your interest. PGo is independent of ShiViz and does not currently output instrumentation for ShiViz (i.e., does not integrate GoVector, which is necessary to get ShiViz-compatible logs from Go output).

I'm curious about your use case behind the question -- are you using PGo for something, or are interested in using PGo?

gedw99 commented 2 years ago

Hey

may use case .. I want to replicate data between clients and servers where the clients can be offline and do mutations .

So ordering of mutations globally, like an event stream.

Logical clocks seems to be they best way .

The data tyoes are: Files , where each mutator only sends the binary diff as the change event; kv with a namespace.

Consul or Etcd would be enough for online , but won’t work for offline.

bestchai commented 2 years ago

Thanks for the description. This (PGo) project might help you with design of your replication logic, but only if you need to have some formal guarantees. For example, if you care about specific ordering properties, then modelling your system in MPCal can checking it with TLC will tell you if the property is true for your model (see this page for more information https://lamport.azurewebsites.net/tla/tla.html ).

Logical clocks are indeed appropriate for reconciling offline mutations. A good example of this are CRDTs, which can help to reconcile copies automatically: https://hal.inria.fr/inria-00609399v1/document

A more classic piece of work in this space is the coda file system: https://dl.acm.org/doi/pdf/10.1145/146941.146942

gedw99 commented 2 years ago

thanks.

for now i don't want to use the scala generator, but instead just test out my golang code that uses github.com/UBC-NSS/pgo/distsys.

I can testout the file and event distribution concepts then.

Then i can loop back to using the scale generator later.

So i just really wanted help in hooking up the tracing GUI.

Does this make sense ?

bestchai commented 2 years ago

I'm going to quote Finn, who thought a bit about your question --

Due to our custom architecture, there isn't so much of a "simple" method of integrating GoVector. Maybe the best approach would be to write a custom driver for GoVector (so, make an additional implementation of Recorder here https://github.com/DistCompiler/pgo/blob/master/distsys/trace/recorder.go and install it with the SetTraceRecorder config option). The problem is that this is more of a prototype feature and so all resources except one variant of TCPMailboxes have their vector clock handling stubbed, meaning by default most programs will just not record any communication (each individual will advance its local clock correctly, but no communication will be visible). The only fix for that is to un-stub the VClockHint method on the desired ArchetypeResource implementations, which might be a high barrier to entry for someone just trying to hack their way through. How annoying that last step is depends on exactly which resources they want to use, though. They might just be lucky.

As Finn notes, it's not an easy task.

Overall, I'd say that we're a bit surprised by your use of distsys since that code is not intended to be used directly by humans, but rather the PGo scala compiler :-)