Re: [tlaplus] Developing a TLA+ Model for the KafkaRoller in the Strimzi Project

Hello,

Maybe this could be a first start on the definition rules:

https://gist.github.com/lkraider/07cef395cc2a648cbaac747fe33d8bf7

There is missing logic on the possible state changes and running this model will fail as there are no restraint rules on them, as I would need to understand the possible state changes and model them accordingly.

So for example running this model:

SPECIFICATION Spec

INVARIANTS
NodesWithinRestartLimit
NodesWithinRetryLimit
ActiveControllerNotRestarted
ControllerQuorumMaintained

PROPERTIES
AllNodesServing
NodesNotStuckRecovering

CONSTANTS
ControllerNodes = {"controller-0", "controller-1"}
BrokerNodes = {"broker-2", "broker-3", "broker-4"}
CombinedNodes = {}
MaxRestartAttempts = 3
MaxRetries = 5

Will hit a failed state fairly quickly because there is no rule that a RESTART can't happen on initialization:

/\ activeController = "controller-0"
/\ nodeState = ( "controller-0" :>
[ state |-> "RESTARTED",
roles |-> {"controller"},
restartAttempts |-> 1,
retries |-> 0 ] @@
"controller-1" :>
[ state |-> "UNKNOWN",
roles |-> {"controller"},
restartAttempts |-> 0,
retries |-> 0 ] @@
"broker-2" :>
[ state |-> "UNKNOWN",
roles |-> {"broker"},
restartAttempts |-> 0,
retries |-> 0 ] @@
"broker-3" :>
[ state |-> "UNKNOWN",
roles |-> {"broker"},
restartAttempts |-> 0,
retries |-> 0 ] @@
"broker-4" :>
[ state |-> "UNKNOWN",
roles |-> {"broker"},
restartAttempts |-> 0,
retries |-> 0 ] )
/\ reconfiguringNodes = {}
/\ restartingNodes = {"controller-0"}

My suggestion on the first step on evolving this spec would be to fix the possible state transitions.

Hope this helps.

att,

--
Paul Eipper

On Fri, Apr 26, 2024 at 7:34 AM Maroš Orsák <maros.orsak159@xxxxxxxxx> wrote:

Hello,

I am writing to seek assistance with developing a model for the KafkaRoller within the Strimzi open-source project, which I maintain. For context, Strimzi is a Cloud Native Computing Foundation (CNCF) project that simplifies the complexities of managing Apache Kafka, a distributed system. The project provides a suite of operators that facilitate various tasks, including updating Kafka clusters, scaling nodes, and integrating multiple components such as tracing and OAuth2, among others.

A critical aspect of managing Kafka clusters is determining when a Kafka node should be rolled. To address this, we have developed a KafkaRoller class. Recently, we proposed a new design featuring an advanced algorithm intended to enhance this functionality. To ensure the safety and correctness of this algorithm, I aim to create a model in TLA+ that will allow us to formally verify it using safety and liveness properties. These properties include but are not limited to, ensuring that no node exceeds maximum retries (safety), preventing the simultaneous restart of all controller nodes (safety), and guaranteeing that all nodes will eventually be in a SERVING state (liveness).

However, I am unfamiliar with how to properly construct such a model and specify these properties in TLA+. Moreover, I lack time to do such a thing...so any guidance or support you could provide would be greatly appreciated. Thank you.

[1] - https://strimzi.io/
[2] - https://www.cncf.io/
[3] - https://kafka.apache.org/
[4] - https://github.com/strimzi/proposals/blob/9a777c320c56e3edd473f088a89864fa643ac63a/06x-new-kafka-roller.md#algorithm

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAMd-2QuocAToKY7HoorcvM8szpMSUu81UzgjRRs9gxROVkUhSg%40mail.gmail.com.