gabrielgiussi / cappio Goto Github PK

Write sequence diagrams to be able to discuss with book's authors about my current implementation and its limitations.

Implement diagrams that won't be backed by modules, just ui actions like Write,Read,Send,Deliver, etc.
This simplifies ui testing and allows us to write freehand diagrams for general purpose.

This could be implemented using a yaml, e.g.

0
  p0
     send A to 1
  p1 
     send A to 0
1 
  p0
    deliver A from 0

I'm not going to show internal requests because that will render a lot of arrows and the diagram will be pretty useless.
But I definitely need to show some internal indications, basically Crash from failure detectors. But I shouldn't show other kinds of internal indications like PLDeliver.

Problem

A Mod has only the indication's type of its direct dependency, so I can't expose crashes for Causal Bcast for example, because the PFD is dependency from the Reliable Bcast.
Maybe with dotty union types, this will be more easy to expose.

Proposal

Create a case class InternalIndication used for all kinds of indications (could be typed with the payload).
If I do only this it will be difficult to create specific representations in SVG for crashes, for example, so maybe I can distinguish a few types of internal indications and use one for general cases.

Create svg text with action type (e.g. beb-bcast) and payload.

I can't show these payloads always because it's hard to have control to avoid them from overlapping.
I can't show the payload only when the user clicks on the corresponding arrow.

But I should also have a way to distinguish sends based on the payload (e.g. bcast vs heartbeats), maybe using different colors.

Changes required

For this, I need to include the payload and the UUID in the action.

These packets can't be dropped so we could deliver them right away.
Can be part of the same step?

A modal should be opened after passing a level (aka achieving all the conditions) and after closing the modal should send me to the next level.

Mdbootstrap has modals but I don't know how to open them from code.

Draw deliver arrows with sender == receiver for broadcast delivers.

Because we are using StubbornLink packets are resend on each tick independently of if they were already delivered or not. This is annoying for the user if he already delivered the packet and only add noise to the diagram.

We need to implement the filter in the UI because in the core we are not able to do it, i.e. the PerfectLink does not see the FLLSend sent by the stubborn and the stubborn can't contain the logic because it doesn't know if the packet was delivered already.

I could add a filter that checks the set of allSent and alreadyDelivered from Network.

Restrict register operations when there is one pending.

"After a process has invoked an operation like this, the register abstraction may trigger an event that carries the reply from the operation. We say that the process completes the operation when this event occurs. Each correct process accesses the registers in a sequential manner, which means that after a process has invoked an operation on a register, the process does not invoke any further operation on that register until the previous operation completes." (pag 138)

mdbootstrap has https://mdbootstrap.com/plugins/jquery/treeview/ but requires animation!

I'm not using them to deliver to the corresponding component because I'm composing modules in a way that I don't have a list of components where I need to find the one with the same instance, I create compositions without losing the types so deliver a message is type safe.
However, could be good to retain the instance to show it in the UI because it is used in the book.

1. From Linearizability versus Serializability
   a. What he means with real-time and later if there are not sync clocks? later in which terms?

   Linearizability is a guarantee about single operations on single objects. It provides a real-time (i.e., wall-clock)
   once a write completes, all later reads (where “later” is defined by wall-clock start time) should return the value of that write or the value of a later write

   b. What it means that linearizability is composable? (I need an example)

   We say linearizability is composable (or “local”) because, if operations on each object in a system are linearizable, then all operations in the system are linearizable.

   c.

   Unlike linearizability, serializability does not—by itself—impose any real-time constraints on the ordering of transactions. Serializability is also not composable. Serializability does not imply any kind of deterministic order—it simply requires that some equivalent serial execution exists.

• https://jantoniomora.wordpress.com/2016/05/28/archivos-para-scorm-funciones-js/
• https://github.com/gabrieldoty/simplify-scorm
• https://www.learnupon.com/blog/scorm-api/
• http://www.dirinfo.unsl.edu.ar/profesorado/PagProy/articulos/5_100_Objetos_de_aprendizaje__Chiarani__Panuchi_.pdf
• https://www.easy-lms.com/knowledge-center/lms-knowledge-center/what-is-an-lms/item10182
• http://sedici.unlp.edu.ar/bitstream/handle/10915/19843/Documento_completo.pdf?sequence=1
• https://app.talentlms.com/create
• https://www.subitus.com/blog/como-funciona-scorm-que-es-manifiesto-sco/#Que_es_un_SCO_Que_es_un_asset

• https://docs.moodle.org/37/en/SCORM_FAQ
• https://pipwerks.com/downloads/
• https://github.com/adlnet/Starting-from-SCORM-A-Developers-Guide/blob/master/Instructions.md
• https://adlnet.gov/public/uploads/SCORM_Users_Guide_for_Programmers.pdf
• http://gamestd.io/scorm/ *
• https://github.com/gamestdio/scorm *
• https://cloud.scorm.com
• https://github.com/arisjulio/scorm-api-adapter
• http://www.unpa.edu.ar/sites/default/files/descargas/Administracion_y_Apoyo/4.%20Materiales/2016/T129/SCORM_Standar.pdf *

https://jepsen.io/consistency

We should add consistency models based on Sebastian Burckhardt's work

Test the usage of State monad.

• https://typelevel.org/cats/datatypes/state.html
• http://rcardin.github.io/design/programming/fp/monad/2018/11/22/and-monads-for-all-state-monad.html
• http://eed3si9n.com/herding-cats/State.html

Levels should be disabled and be enabled only after previous one was passed.
I have an implementation for the logic but the element doesn't understand the disabled attribute.

I'm currently using shapeless Coproducts but maybe this is a simpler solution (until scala 3)

We need to enforce packet delivery to comply with synchronous model constraints to support fail-stop algorithms.

Proposal

Solution for PerfectFailureDetector

Remove the restriction of one delay per process per turn, this will allow receiving heartbeats from N processes in the same round.
So, instead of having

request -> tick -> deliver -> tick

We'll have

request -> deliver -> deliver -> ... -> deliver  -> tick

Why N deliver step instead of having a single one that allows N delivery per process? Because we must still provide a way to define the order of deliveries to the user and with this solution, he will not be able to see how each delivery affects state.

Since we deleted the tick between request and deliver (*) we need to filter the packets sent in the request stage to the delivery stage in the same step. For this, the tick should also increase a counter in the Network object, so we can mark the packets with the step when they were sent and know which is the current one, then we can only show as available packets those with step < current

(*) When to tick?

I still don't know how impacts this change to the correctness of the algorithms, it's not clear for me when I must tick, understanding tick as the moment to validate conditional event handlers an increasing counters used for timeouts as in PerfectFailureDetector and StubbornLink.

Enforcing network bounded delay

Regarding the network bounded delay, it will not be implemented in the scheduler and is going to be a condition that users must accomplish. For this, I need to mark when packets were sent and which is the current turn.

Investigate if this in-memory database that allows write queries using datalog is a good option to write conditions.
The idea is to write requests, indications, drops, etc as facts and then write queries for complex conditions.
I don't know if there is an easy way to write the state of the abstraction's stack (e.g. beb-pl-st) as facts also.

There is also a sql option

1. How to throttle key press?

   inContext(thisNode => onChange.mapTo(Option(thisNode.ref.value).filterNot(_.isEmpty).map(p => BebBcast(Payload(p),Instance("")))) --> obs)
   

2. How to clean a form after submit?

3. WriteBus vs Observer?

4. Var update vs set vs setCurrentValue

5. How to trigger a dom event, e.g. change hash for routing.

It should be used to enable further levels and also from the oa to tell the LMS when the sco is finished

When a new level is started (should be the first time you open a level) the full descriptions of the conditions should be shown with a short description of the level's goal, e.g. "In this level we are going to use the broadcast to send a message to all processes of the cluster".

We should be able to draw this software stacks automatically from the composition used in each level (not with the current implementation but seems doable)

At least we should be able to create a function using scala-dom-types that receives the structure of the composition and returns an svg()

Operation vs Value

I can implement both and the difference will appear mainly in the messages. I can't use this difference for conditions because in order for this to make sense I should enable the user to select with kind of abstraction wants to use and add some conditions that take into account the "weight" of the messages or stablish a delay based on this "weight".

I need to understand two things:

1. in which moments I will do the prepare and effect stages.
2. if I require another abstraction on top of CausalBroadcast (eventuate has an event log).
3. crdts requires vector clocks or version vectors? (eventuate uses plausible vector clocks)

Read

• Version vectors are not vector clocks
• Eventuate vector clocks
• https://www.coursera.org/learn/cloud-computing/lecture/dy8wf/2-5-vector-clocks
• Why Logical Clocks are Easy

Pure Op

I think this mainly changes the internal implementation that the user will not be able to see. So maybe it only makes sense to implement an abstraction with both pure + stable.

Pure Op + Stable

This requires the causal broadcast abstraction to expose the vector time in the CRBDeliver. Is easy to expose always and only use it in the app abstraction that does stabilization.
Read

• Making operation based CRDTs operation based or Pure Operation-Based Replicated Data Types
• Switch to pure operation-based CRDTs
• Eventuate PR

"It is convenient for presentation simplicity to assume the existence of a global clock, outside the control of the processes. This clock provides a global and linear notion of time that regulates the execution of the algorithms. The steps of the processes are executed according to ticks of the global clock: one step per clock tick.Even if two steps are executed at the same physical instant, we view them as if they were executed at two different times of our global clock. A correct process executes an infinite number of steps of its automaton, i.e., every such process has an infinite share of time units (we come back to this notion in the next section) and follows the specified algorithm. In a sense, there is some entity, sometimes called a global scheduler, that assigns time units to processes, though the very notion of time is outside the control of the processes.
A process step consists of receiving (sometimes we also say delivering) a message from another process (global event), executing a local computation (local event), and sending a message to some process (global event)" (pag 21).

Is related to #12

Lamport clocks increments with the following (abstract) events

• send a message
• receive a message
• local processing

For us

• receive can be the delivery
• Is local processing only requests?

Questions

• Who increments the Lamport clock? Is a new abstraction layer above PerfectLink?
• With the option above we could increment the clock on sends and deliveries, but what about local events like requests?
• If I have an abstraction that uses is composed of two different ones, it will have two different Lamport clocks. (This also happens with causal past if I use two different causal broadcast abstractions)

Documentation

• https://medium.com/baseds/logical-time-and-lamport-clocks-part-1-d0317e407112

With the current implementation I can't plugin different implementations of an abstraction into AbstractModule.
For example I want to instantiate two different implementations of the Best Effort Broadcast module, one using a PerfectLink and another one using a SmartPerfectLink (doesn't resend the packet if it was already delivered, mainly for getting a cleaner diagram).
For this, I want to define the type

type PublicBeb = Mod {
  type Req
}

However I can't build Modules with the following function

  def mod2[M <: ModS[Dep], Dep <: Mod](initial: M#S, p: ProcessLocalM[M, Dep]): Module[Mod {
    type Req = M#Req
    type Ind = M#Ind
    type Payload = M#Payload
    type State = M#S
  }] = {
    case class InternalModule(s: M#S) extends AbstractModule[M, Dep] {
      override def copyModule(state: M#S): AbstractModule[M, Dep] = copy(state)

      override val processLocal: PLocal = p

      override def state: M#S = s
    }
    val i = InternalModule(initial)
    type NewType = Mod {
      type Req = M#Req
      type Ind = M#Ind
      type Payload = M#Payload
      type State = M#S
    }
    new Module[NewType] {
      override def request(in: M#Req): Next = i.request(in)

      override def state: M#S = i.state

      override def tail = i.tail

      override def tick: Next = i.tick
    }
  }

But Module is invariant in M so tick must return a NextState[M] and not some type even if it has the same type members.

[error]  found   : internal.Next
[error]     (which expands to)  oss.giussi.cappio.NextState[M]
[error]  required: this.Next
[error]     (which expands to)  oss.giussi.cappio.NextState[oss.giussi.cappio.Mod{type Req = M#Req; type State = M#S; type Ind = M#Ind; type Payload = Dep#Payload}]
[error]       override def tick: Next = internal.tick

The whole solution is, hence, useless because I cannot plugin different abstractions.
I don't know if the limitation comes from using the trait Mod that has the type members or if that is ok and the problem comes from ModS.

The goal of trait Mod is to capture the relationship between Requests, Indications, State and Payload and have access to these types to build new types with shapeless (for CombinedModule for example)

Without this, I can't implement a SmartPerfectLink that (see #46) doesn't resend packets that were already delivered. The idea is to have a single abstraction that combines the logic from PerfectLink (dedup) and StubbornLink (resend) but if I change this type I need to propagate the change to all abstractions because it changes the type of the dependency.
A quick solution could be have two BestEffortBroadcast one with StubbornLink to explain stubborn links and another one with the SmartPerfectLink that will be reused for all remaining abstractions.

• Level 1 (simple beb): beb deliver value [A] to all processes

  • Trigger single Bcast (requires access to requests)
  • All processes should be UP (requires access to processes status)
  • All processes should bebdeliver [A] (requires access to process state (*) or indications)
  • Drop a message (this actually doesn't show a guarantee provided exclusively by the beb but by the stubborn link, but still may be good to show it in action). Also, this could be (as a posterior enhancement) a "network partition" introduced by the level and not by the user (for now I don't have this feature implemented).
    

• Level 2 (break beb): beb doesn't guarantee the delivery to all correct (aka alive) processes when sender fails.

  • Process 1,2,3 with state [AC]
  • Process 4 with state [C]
  • No messages left to deliver (**)
  • Make only two bcast from any process
  • The conditions above should force the need to kill the sender, if not add extra conditions.
    

• Level 3 (fix beb with rb)

  • All correct processes must have state ABC
  • Process 1 should crash in the second step (***)
  • Process 1 state should be A
  • Process 1 must send the bcast of A
  • (I should add another process crash so it requires more interaction from the user)
    

• Level 4 (break rb): not all processes agree in the same set of messages
  

• Level 5 (fix rb with urb): each process delivers the message only when all correct processes have seen the message
  

• Level 6 (break urb - no order guarantees)

• Level 7 (FIFO bcast)

• Level 8 (break fifo - no causality)

• Level 9 (causal bcast)

• Level 10 (break causal - no total order)

• Level 11 (crdt - solve conflicts)

(*) I don't have implemented a way to access process state, I tried to add an abstraction that behaves as the app layer with a state that is updated with each bebdeliver (and I can maintain a list of the values saw or just the last one) but what will be the shape of that abstraction?

AppMod[P] = ModS[BebMod[P]] {
   type Ind = AppInd // because I need this abstraction to still trigger the indication so I can draw it
   type Req = BebBcast // and just forward?
   type S = AppState[P]
}

The other option is to add state in oss.giussi.cappio.Process and add a function

(M#Ind,State) => State

(**) This is related to a liveness guarantee so is harder to test. In this case because beb is using a stubborn link so is guaranteed that even if some messages are dropped the message will be broadcasted unless the sender failed. So, to check this condition I need to search for all alive processes and see their stuborn link's state to see which messages are going to be re-send, but also see which messages were already delivered.

val alive = processes.filter(status = alive)
val to-resend = alive.map(_.stubborn.state.sent) // stubborn always resend all messages
val delivered = indications.filter(ind = PLSend)
val are-messages-to-deliver? = (to-resend -- delivered).isNonEmpty

(***) For this kind of condition I would need to index requests, indications, crashes and drops.