Awesome work Jack!
I haven't worked with formal verification but have always been interested.
Can you share the tools, thinking processes, setup etc that went into this?
On Mon, Feb 22, 2021 at 9:19 AM Jack Vanlightly
wrote:
> Hi all,
>
> I have written a TLA+ specification for the replication
Hi all,
I have written a TLA+ specification for the replication protocol. It models
the life of a single ledger and includes two writers, the original writer
that creates the ledger and a second writer that can at any point (or not)
start the recovery process.
It found one problem with the fencin
I forgot to add that I tested also the RC binaries against HerdDB,
everything worked like a charm
Enrico
Il giorno lun 22 feb 2021 alle ore 14:52 Enrico Olivelli <
eolive...@gmail.com> ha scritto:
> +1 (binding)
> - Verified RAT,Spotbugs,Checkstyle...
> - Verified signatures and digests
> - Buil
Hello Bookkeeper Community,
I am looking to add an alert on my bookkeeper's metrics so I can know when
the number of underreplicated ledgers goes above 0. (If there is already a
good way to do that, I'm open to suggestions. I don't want to run any
commands against the cluster, though. I'd like to
+1 (binding)
- Verified RAT,Spotbugs,Checkstyle...
- Verified signatures and digests
- Built and Run tests on Ubuntu+JDK8 (no integration tests). I created a
few issues about flaky tests on DLog (the build passed because we have auto
retrial on failures)
- Run smoke tests on JDK8 with localbookie a
