Global Variable and Non Termination

[mohit jangid]

Hi All,

When modeling global variables, often a single state fact is maintained across rules as shown below: 

rule rule_use :

    [Global_var(value), 

           ..

    ]

  --[ ]->

    [Global_var(value), 

    ..    

    ]

rule rule_update:

    [ Global_var(value),

      State_fact(value2)

      .. 

     ]

  --[ ]->

    [Global_var(value2), // update global var to value2

     ..

    ]

  

However, such modeling often creates loop breakers and some proofs do not terminate due to multiple recursive sources of Global_var fact. 

Is there any alternative way or safe way to model the global variables? 

Thank you

[Benjamin Kiesl]

Hi Mohit,

You can try modelling a mechanism similar to pointer allocation/deallocation in high-level programming languages. The intuitive idea is that for your "global variable" you create persistent facts that have two parameters: (1) the memory address (the "pointer address") of the variable and (2) the value of the variable. Then, whenever you want to "update" your variable, you actually free the old memory and allocate new memory. You just have to make sure that your pointers cannot be accessed after their memory has been freed and that memory cannot be freed more than once (which you can do with restrictions).

The following example illustrates how this could be formalized in Tamarin:

================================

restriction FreedMemoryCannotBeAccessed:
    "All pointer #i #j. Read(pointer) @ i & Free(pointer) @ j ==> i < j"

restriction MemoryCanBeFreedOnlyOnce:
    "All pointer #i #j. Free(pointer) @ i & Free(pointer) @ j ==> #i = #j"

rule rule_create:
    [ Fr(~pointer), ... ]
    --[]->
    [ !GlobalVariable(~pointer, value) ]

rule rule_use:
    [ !GlobalVariable(~pointer, value), ...  ]
  --[ Read(~pointer) ]->
    [ ... ]

rule rule_update:
    [ !GlobalVariable(~oldPointer, oldValue), Fr(~newPointer), ...  ]
  --[ Free(~oldPointer) ]->
    [ !GlobalVariable(~newPointer, newValue) ]

================================

Note that the rule "rule_use" is not recursive, as the persistent fact !GlobalVariable occurs only on the left-hand side. Also, in the rule "rule_update", both ~oldPointer and ~newPointer are fresh, meaning that they are not E-unifiable (and thus the rule is not recursive in a strict sense).

Cheers,
Benjamin

--
You received this message because you are subscribed to the Google Groups "tamarin-prover" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tamarin-prove...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tamarin-prover/051790a7-9631-4bdd-b744-4b520efba781o%40googlegroups.com.

[mohit jangid]

Thank you, Dr. Kiesl. This is very helpful.  

To unsubscribe from this group and stop receiving emails from it, send an email to tamarin...@googlegroups.com.

[mohit jangid]

Hi All,

Building upon the pointer version of the global variable, I am trying to establish stronger properties for global variable implementation. The property is -- every read and free action borrows pointer and value either from the last recent free action or create (setup) rule. 

I have attached a file <global_var_ptr.spthy> with a simple protocol using global variables. The desired properties are present in lemmas -- each_freeG_borrows_lastestG and each_readG_borrows_lastestG. 

I have tried different variations of these lemmas and I am studying the Tamarin induction proof concept in order to establish the properties. However, I am not able to prove these lemmas yet. The manual GUI proof investigation reveals that the present lemma generates recursive subcases that are not captured as a part of the induction step or cyclic contradiction. 

I would appreciate any help in help/guidance in this direction. Please let me know I shall provide more clarification for the problem or the simple protocol present in the attached Tamarin file.

Thank you