Bounded spaces

[albertolluch]

All spaces classes we provide have unbounded capacity. I propose we consider a parameter to optionally make them of bounded capacity.

Bounded spaces have several applications (e.g. devices with limited resources, too fast producers that need to be contained...) and can make things easier (even decidable) for verification (e.g. Spin/Promela channels are bounded channels).

In a bounded space, the put operation blocks if the space is full.

@michele-loreti @sequenze @luhac objections?

PS. For capacity 1 all spaces would have the same behaviour.
PS2. One could even consider capacity 0 implement synchronous rendezvous: queries always fail, put and get synchronise. But, for now, capacity > 0 is all I propose.

[sequenze]

This sounds neat. I like this :)

[ghost]

No objections, only questions:

1. How is the capacity of the space measured in (tuple count, bytes (in embeded systems, this would be relevant) or something else)?
2. Do we discriminate an n-tuple by its size n (relevant if the tuple space is measured in bytes)? Say, in embedded devices, smaller tuples are prioritised more than large tuples.
3. What is the semantics of putp? Where do we store a tuple between two peers:
   a. That are connected to each others bounded space.
   b. Both spaces are full.
   Do we follow a strategy for as for put and block?
   Queue tuple up somewhere and continue?
   Drop the tuple?

@albertolluch
I sense that you are suggesting something in the lines of having a Capacity interface for specifying how large a bounded space would be:

int n = 42;
Capacity c = new Storage(n);
BoundedSpace b = new BoundedSpace(c);

Given the discussion in #5, I have a few suggestions.

For describing a bounded space by tuple count, one could define a bounded space as follows:

int n = 42;
Capacity c = new Storage(n);
Space s = new Space(c);

For an unbounded space, then:

Capacity c = new Unbounded();
Space s = new Space(c);

In my opinion, by default, Space s = new Space(); should be an unbounded space where semantics of operations are not changed. Reason is that given many mobile entities (smartphones, laptops, tablets) and workstations where API will see usage, storage space is not a concern.

For bounded spaces (and in tight environments where this could be useful: small IoT devices, sensor networks, ensembles etc.) one could see the use of a capacity strategy.

Imagine the following case: a sensor network in a remote area, and where one wants to avoid deadlocks and in exchange accept loss of information.

Initialisation for each node in such a network could be:

int n = 1024;
CapacityStrategy cs = new DropCapacityStrategy();
Capacity c = new StorageCapacity(n, cs);
Space b = new Space(c);

This initialises a bounded space of capacity of 1024 tuples, and when full, will drop tuples on non-blocking operations that add more tuples to the space. Any semantics of blocking operations are not changed by CapacityStrategy.

Default CapacityStrategy for StorageCapacity when using non-blocking operations should be to queue tuples, say, via QueueCapacityStrategy.

As of current writing, I am not aware of small embedded systems that could host any of the current Space API implementations, and therefore I do not see a reason to have a strategy to drop data as default via a DropCapacityStrategy. A BlockCapacityStrategy that alters non-blocking operation semantics could be useful, but should only be used in scenarios where it is meaningful in order to avoid a deadlock nightmare.

@albertolluch @michele-loreti @sequenze What do you think?

[albertolluch]

thanks @luhac, interesting ideas.

How is the capacity of the space measured in (tuple count, bytes (in embeded systems, this would be relevant) or something else)?

For now only tuple count, to adhere to well-understood notions of bounded channels. In the future we may considering more sophisticated notions.

What is the semantics of putp?

It is not part of the core API.

For bounded spaces (and in tight environments where this could be useful: small IoT devices, sensor networks, ensembles etc.) one could see the use of a capacity strategy.

This is a very interesting idea to pursue in the future. It would require to study first a clean formalisation.

In sum, I propose that for now we stick to a simple notion of bounded space based on number of tuples that can be stored. As I said, this has the unique advantage of being able to use model checking tools for modelling and verification.

[albertolluch]

The formal semantics of bounded spaces is now specified here:

https://github.com/pSpaces/Programming-with-Spaces/blob/master/semantics.md

We should mark here which implementations do not (yet) supporting bounds.

https://github.com/pSpaces/Programming-with-Spaces/blob/master/naming.md