PropER generator for list of records with a sequence number

classic Classic list List threaded Threaded
7 messages Options
Reply | Threaded
Open this post in threaded view
|

PropER generator for list of records with a sequence number

Frans Schneider-2
Hi list,

In PropER, I am looking for a way to generate records with one field
being a sequence number which is incremented for each instance.

-record(cache_change, {sequence_number :: sequence_number(),
                       ...
                       data_value :: term()).

Every cache entry is supposed to have a new sequence number which is
normally generated by the application, but I now want PropER to generate
the sequence numbers to test drive the cache in isolation.

How does one create a custom generator for this?

Another, related question, is how to start an unregistered process (the
cache) in PropER and use its pid? Normally, the caches are started from
a simple-one-for-one supervisor. The cache should be restarted for every
test run. PropER documentation and examples always show registered
processes and not unregistered processes.

Thanks,

Frans
_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: PropER generator for list of records with a sequence number

Torben Hoffmann
Hi Frans,

This will most likely run you into some problems with shrinking.
You would have to generate the next sequence number from the previous one, but then no shrinking can be done since that would leave a gap in the sequence numbers.
But maybe there is another way to do this that I can't think of right now.

Cheers,
Torben

On Mon, 10 Dec 2018 at 08:30, Frans Schneider <[hidden email]> wrote:
Hi list,

In PropER, I am looking for a way to generate records with one field
being a sequence number which is incremented for each instance.

-record(cache_change, {sequence_number :: sequence_number(),
                       ...
                       data_value :: term()).

Every cache entry is supposed to have a new sequence number which is
normally generated by the application, but I now want PropER to generate
the sequence numbers to test drive the cache in isolation.

How does one create a custom generator for this?

Another, related question, is how to start an unregistered process (the
cache) in PropER and use its pid? Normally, the caches are started from
a simple-one-for-one supervisor. The cache should be restarted for every
test run. PropER documentation and examples always show registered
processes and not unregistered processes.

Thanks,

Frans
_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions


--

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: PropER generator for list of records with a sequence number

Paul Peregud-2
Possible solution - move id assignment out of the generator into a thin wrapper around SUT.

On Mon, Dec 10, 2018 at 7:59 AM Torben Hoffmann <[hidden email]> wrote:
Hi Frans,

This will most likely run you into some problems with shrinking.
You would have to generate the next sequence number from the previous one, but then no shrinking can be done since that would leave a gap in the sequence numbers.
But maybe there is another way to do this that I can't think of right now.

Cheers,
Torben

On Mon, 10 Dec 2018 at 08:30, Frans Schneider <[hidden email]> wrote:
Hi list,

In PropER, I am looking for a way to generate records with one field
being a sequence number which is incremented for each instance.

-record(cache_change, {sequence_number :: sequence_number(),
                       ...
                       data_value :: term()).

Every cache entry is supposed to have a new sequence number which is
normally generated by the application, but I now want PropER to generate
the sequence numbers to test drive the cache in isolation.

How does one create a custom generator for this?

Another, related question, is how to start an unregistered process (the
cache) in PropER and use its pid? Normally, the caches are started from
a simple-one-for-one supervisor. The cache should be restarted for every
test run. PropER documentation and examples always show registered
processes and not unregistered processes.

Thanks,

Frans
_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions


--
_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions


--
Best regards,
Paul Peregud
+48602112091

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: PropER generator for list of records with a sequence number

Jesper Louis Andersen-2
In reply to this post by Frans Schneider-2
On Mon, Dec 10, 2018 at 8:30 AM Frans Schneider <[hidden email]> wrote:
Hi list,

In PropER, I am looking for a way to generate records with one field
being a sequence number which is incremented for each instance.


This is somewhat haphazard, you have been warned!

Some questions/initial guesses:

* If you run 100 proper tests, do you want the cache to be restarted 100 times, or just once? The former does not provide any kind of isolation between runs, which is usually not what you want to do.
* Use `erlang:unique_integer` to provide a unique integer for each run, and feed it into the cache?
* It isn't entirely clear what a run means to you, and what property you are trying to epoch-test.
* If you have any kind of relations between commands toward your cache, you can look at stateful testing.
* By "not entirely clear" I mean that the lifetime needs of your SUT and your test generator isn't really known to us.

Some observations:

* Observation: the seqno is "time". Time should often be injected.
* Create your cache so you can start it with a given seqno. Feed this into the cache by injecting it as a parameter when you start it.
* Your cache run can then assume that seqno.
* If you go for a stateful test, you can then write properties which verifies the cache handles its seqno correctly, for all possible starting seqno.
* Write a test where there is only a single key. Focus on the seqno since that is highly likely to contain an error. Once you have this, extend your model with multiple keys, but keep it low: 2 to 5 keys should be more than enough to capture almost all kinds of errors in the system.

In a stateless model, the best you can do is generating random integers as sequence numbers and verify the cache does the right thing given its current state. Say it should ignore updates if a sequence number is too low. Then if we start with a large integer in the sequence, then most runs will just reject the input, as it should. In a stateful model, you can track the state of the cache and then generate sequence_numbers with the property they are monotonically increasing, which will make the system test the "real code". A stateful model would also fault-inject once in a while to test the case where the sequence number is too low.

One big advantage of the stateful model is precision: when failure occurs, it knows the command sequence which made the failure occur, so it can often point to the culprit by shrinking. A stateless model needs to search more to find the problem. The disadvantage is that a stateful model requires more work to implement and get right.

Personally, I'd just go with a stateful model immediately. Add a way to query your cache for its current contents. Then you can write your update commands such that they update, then query the cache state. This makes postconditions/invariants easy to write for the system. Start with a single command and work from there. As you add commands, you will start to find the problems in the SUT. I.e., the first goal should be to initialize the cache and then ask how large it is or something such. This should always be 0. Then stop the cache again. Next model could track if you updated a single key in the cache or not. So the size is either 0 or 1, depending on when that call happens. You can slowly extend the model from this simple initial idea until you cover everything.

IF you want to go with a stateless model, generate a random list of operations to run against the cache. Run these against the cache and against a different local model you have. Then run an observation against both and fail if they don't agree. This provides isolation from run to run (your 100 test cases might run 10 cache operations each, roughly). However, many operations will not have effect, and the observations will be weaker than a stateful model, so you would have to do more runs before you hit a problem.


_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: PropER generator for list of records with a sequence number

Frans Schneider-2
Thanks guys for the suggestions.
I guess I'll have to add some extra code for starting and stopping the
cache and generating the cache changes that PropER can use. I don't want
to make changes to the application's code base to facilitate testing
because that would give to much clutter.
I'll also go for the stateful approach as suggested.
PropER is great, but it takes some time to get used to it...

Frans


On 12/10/18 12:18 PM, Jesper Louis Andersen wrote:

> On Mon, Dec 10, 2018 at 8:30 AM Frans Schneider <[hidden email]
> <mailto:[hidden email]>> wrote:
>
>     Hi list,
>
>     In PropER, I am looking for a way to generate records with one field
>     being a sequence number which is incremented for each instance.
>
>
> This is somewhat haphazard, you have been warned!
>
> Some questions/initial guesses:
>
> * If you run 100 proper tests, do you want the cache to be restarted 100
> times, or just once? The former does not provide any kind of isolation
> between runs, which is usually not what you want to do.
> * Use `erlang:unique_integer` to provide a unique integer for each run,
> and feed it into the cache?
> * It isn't entirely clear what a run means to you, and what property you
> are trying to epoch-test.
> * If you have any kind of relations between commands toward your cache,
> you can look at stateful testing.
> * By "not entirely clear" I mean that the lifetime needs of your SUT and
> your test generator isn't really known to us.
>
> Some observations:
>
> * Observation: the seqno is "time". Time should often be injected.
> * Create your cache so you can start it with a given seqno. Feed this
> into the cache by injecting it as a parameter when you start it.
> * Your cache run can then assume that seqno.
> * If you go for a stateful test, you can then write properties which
> verifies the cache handles its seqno correctly, for all possible
> starting seqno.
> * Write a test where there is only a single key. Focus on the seqno
> since that is highly likely to contain an error. Once you have this,
> extend your model with multiple keys, but keep it low: 2 to 5 keys
> should be more than enough to capture almost all kinds of errors in the
> system.
>
> In a stateless model, the best you can do is generating random integers
> as sequence numbers and verify the cache does the right thing given its
> current state. Say it should ignore updates if a sequence number is too
> low. Then if we start with a large integer in the sequence, then most
> runs will just reject the input, as it should. In a stateful model, you
> can track the state of the cache and then generate sequence_numbers with
> the property they are monotonically increasing, which will make the
> system test the "real code". A stateful model would also fault-inject
> once in a while to test the case where the sequence number is too low.
>
> One big advantage of the stateful model is precision: when failure
> occurs, it knows the command sequence which made the failure occur, so
> it can often point to the culprit by shrinking. A stateless model needs
> to search more to find the problem. The disadvantage is that a stateful
> model requires more work to implement and get right.
>
> Personally, I'd just go with a stateful model immediately. Add a way to
> query your cache for its current contents. Then you can write your
> update commands such that they update, then query the cache state. This
> makes postconditions/invariants easy to write for the system. Start with
> a single command and work from there. As you add commands, you will
> start to find the problems in the SUT. I.e., the first goal should be to
> initialize the cache and then ask how large it is or something such.
> This should always be 0. Then stop the cache again. Next model could
> track if you updated a single key in the cache or not. So the size is
> either 0 or 1, depending on when that call happens. You can slowly
> extend the model from this simple initial idea until you cover everything.
>
> IF you want to go with a stateless model, generate a random list of
> operations to run against the cache. Run these against the cache and
> against a different local model you have. Then run an observation
> against both and fail if they don't agree. This provides isolation from
> run to run (your 100 test cases might run 10 cache operations each,
> roughly). However, many operations will not have effect, and the
> observations will be weaker than a stateful model, so you would have to
> do more runs before you hit a problem.
>
_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: PropER generator for list of records with a sequence number

Jesper Louis Andersen-2
On Mon, Dec 10, 2018 at 1:03 PM Frans Schneider <[hidden email]> wrote:
 I don't want to make changes to the application's code base to facilitate testing
because that would give to much clutter.
 
I'd beg you reconsider this stance.

In my experience, adding tooling around an application in order to query its internal state in a well-defined way is often beneficial when there is a bug and you need to introspect the code in question. Debugging is often helped by having a canonical way to inspect and analyze the application. Also, if you need to run through hoops before you can test your code, chances are you are looking at the wrong API, so it should at least be entertained a better one might exist.

In linear logic, there are two kinds of choice called "additive conjunction" and "additive disjunction". One type, conjunction, is controlled by either the PropER model or by the caller into the application/SUT. The other kind of choice, disjunction, is made by the application/SUT internally when it executes. Additive disjunctions are hard because they make the model unable to predict what will happen. So it has to guard against all types of outcome from the SUT/application, and this makes the models quite weak. The Wikipedia page has a nice example with a vendoring machine interpretation of the model[0], but the idea of a linear dialogue between a buyer and a vendoring machine is exactly mapped into an API user and the process behind the API, implementing it.

One important point about PropER testing is that you must try to shift as much choice to be controlled by the model. This often requires an API where one can inject parameters from the outside to control the setup of certain states. You can always have a sane default which initializes if not overriden, and this is what I've often done. Important examples are that randomness and time must be controlled from the outside in some way. Otherwise, the system tend to become impossible to test. And it also hides important details to the user of the API to boot.


_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions
Reply | Threaded
Open this post in threaded view
|

Re: PropER generator for list of records with a sequence number

Fred Hebert-2


On Mon, Dec 10, 2018 at 4:29 PM Jesper Louis Andersen <[hidden email]> wrote:

One important point about PropER testing is that you must try to shift as much choice to be controlled by the model. This often requires an API where one can inject parameters from the outside to control the setup of certain states. You can always have a sane default which initializes if not overriden, and this is what I've often done. Important examples are that randomness and time must be controlled from the outside in some way. Otherwise, the system tend to become impossible to test. And it also hides important details to the user of the API to boot.

One of the tips I recommend on propertesting.com is to use shim modules. If the API is not  amenable to good control, the generator of the model at least has to be.

So you might have a single call to "add_item(Id, Name, ...)" but various reactions according to whether the item exists or not. The shim module will act as a wrapper where you can instead expose calls like "add_existing_item(...)", "add_unknown_item(...)", or "add_malformed_item(...)". The generator, preconditions, next_state, and postconditions callback can then build their expectations based on the type of operation even though the underlying system handles calls by itself. It also makes it easier to make calls synchronous or asynchronous as long as the underlying system exposes them. It also helps to do things like change a successful return value that you want to store in the state from {ok, Pid} to just Pid, and then pass it back to the next generated call such that it won't clash with the opaque placeholders the framework uses.

this does require the system under test to have at least some level of control given to build this higher-level test-only abstraction, but it helps make things simpler.

The one case I can think of where you may want to adapt your system is when it comes to timeout handling. Ensuring some calls timeout while succeeding or failing is rather difficult and may not always work with a shim, especially in async interfaces. For those, having a way to configure or override timers might be necessary.

But I would also like to violently agree with the notion that the model has to drive the test, which implies that you can, without looking at the system (aside from opaque types like generated IDs that you store in placeholders), create a full predictable execution with useful invariants to check. This can quickly become tricky when you have some non-deterministic results (N/M requests might be dropped), so you have to be careful.

_______________________________________________
erlang-questions mailing list
[hidden email]
http://erlang.org/mailman/listinfo/erlang-questions