Spinroot

A forum for Spin users

You are not logged in.

#1 2019-03-07 18:31:24

maryam
Member
Registered: 2012-03-27
Posts: 16

Model is too large

Hi,

I am modeling a quasi-synchronous system, which consists of several processes, and processes communicate through channels. I have modeled each process similar to the controller process in the following. Every process is activated periodically, reads all messages in its inbox channels atomically, do local computation, and publishes messages. Publishing messages to different channels can be interleaved by other processes execution. To model the interleaving between a message publish and its delivery, I am using two separate channels. commchan_topicname maintains messages published but not delivered yet, and ch_topicname shows the inbox of a process for that topic. There is also a process called deliver, which nondeterministically delivers a message to a process inbox (removes a message from commchan_topicname and sends it to ch_topicname). The model has four such processes plus the deliver process, and it consumes a lot of memory, while it seems simpler than that, as I have wrapped most sequences in a d_step block. Any idea what is wrong in my model, which causes significant memory consumption?

proctype ControllerP()
{
  bool indngr = false;
  short pwr = 10;

  do
  :: len(ch_danger) >= cont_danger_min && len(ch_speed) >= cont_speed_min && len(ch_go) >= cont_go_min ->
    d_step {
      read_chan(ch_danger, local_bfr_danger, cont_danger_size);
      read_chan(ch_speed, local_bfr_speed, cont_speed_size);
      read_chan(ch_go, local_bfr_go, cont_go_size) };
    d_step { step_controller(); };

    len(ch_power) + len(commchan_power) < act_power_size ->
      d_step { publish(tpcPowerId, pwr); };
    len(ch_indanger) + len(commchan_indanger) < opt_indanger_size ->
      d_step { publish(tpcIndangerId, indngr); };
  od;
}

Offline

#2 2019-03-08 01:19:47

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Model is too large

How large are the channels?  The size of channels can have a significant impact on verification complexity.
You're not showing the complete model, so it's hard to tell what the main cause is. Are there counters that could be given a smaller range? How many processes? etc.

Offline

#3 2019-03-08 02:24:43

maryam
Member
Registered: 2012-03-27
Posts: 16

Re: Model is too large

I see, so probably it is the channels. I have 5 processes and 10 channels, four of which has size 7, two has size 3, and four has size 1. There is only one counter that is either 0 or 1.

I guess one solution to decrease the model size is using arrays instead of channels and implement send and receive for them as d_steps. I appreciate if you have a better suggestion?

Last edited by maryam (2019-03-08 02:38:25)

Offline

#4 2019-03-08 19:41:42

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Model is too large

I would recommend trying to reduce the number of channels and/or the size of the channels.
If you can replace a buffered channel with a rendezvous channel, that will also have a big effect.

Offline

#5 2020-08-23 22:20:27

Maxvonhippel
Member
Registered: 2019-09-13
Posts: 20

Re: Model is too large

My experience so far has been that the following techniques reduce model size:

1. Whenever possible use rendezvous communication, i.e., use channels with size 0 instead of size > 0.
2. Minimize the number of channels even if this means increasing the number of possible symbols to be sent over a channel.  For instance, if you have A and B processes, with A sending ack to B and B sending ack to A over two channels AtoB and BtoA, you could reduce this to one channel AandB and have messages ack_from_A and ack_from_B.
3. As much as possible encode logic using labels and goto statements instead of higher-level (more C-like) constructs.  So, loosely, try to make the code look more like assembly, and less like C.
4. Use mtypes instead of shorts/integers/doubles/etc. as much as possible as they force you to clarify your ideas in as finite of a manner as you can.

Would you agree with all this advise?  Are there any other general tips you would reccomend?

Thank you!

Offline

Board footer

Powered by FluxBB