TUM - Chair VII - Foundations of Software Reliability and Theoretical Computer Science


	jMoped - FAQs

Question 1: What is jMoped annotations?

Answer: Because jMoped is slow with integers that have many bits, jMoped annotations give you more control to tell which variables should have which bits apart from the default value on the plug-in view. See What is the annotation @PDSBits?.

top

Question 2: How can I use jMoped annotaions?

Answer: You need to include pds.jar into your classpath. Goto Project -> Properties, select Java Build Path on the left, and then the tab Libraries in the middle. Click Add External JARs... and add the file Moped/jmoped/lib/pds.jar.

top

Question 3: What is the annotation @PDSBits?

Answer: The annotaion @PDSBits is used for specifying bits of fields, parameters, local variables, and array elements. You will have to add pds.jar into your classpath, and import the class PDSBits.

    import de.tum.in.jmoped.annotation.PDSBits;

Usage:

Fields: put @PDSBits just before field declarations. For example,
```
    @PDSBits({"2"})
    int a;
```
the field a will have two bits.
Parameters: put @PDSBits just before method declarations. There are two possibilities to refer to parameters: (1) by sequence (2) by name. To refer by sequence you need to give the bits in the same order as they appear in the method. For example,
```
    @PDSBits({"1", "2"})
    void m(int x, int y)
```
x and y will have 1 and 2 bits, repectively. Alternatively, you can refer to variables by names, e.g.
```
    @PDSBits({"y=2", "x=1"})
    void m(int x, int y)
```
which yields the same result as above.
Local variables: put @PDSBits just before method declarations and refer to the variables by their names, as in the case of parameters. For example,
```
    @PDSBits({"z=1"})
    void m() {
      int z;
    }
```
z will have 1 bit.
Array elements: put @PDSBits just before method or field declarations and refer to the variables by their names followed by []. For example,
```
    @PDSBits({"u[]=1", "v[]=2"})
    void m(int[] u) {
      int[] v;
    }
```
each element of the arrays u and v will have 1 and 2 bit, respectively.

Remark:

@PDSBits always takes an array of Strings as the only argument, and has no comma at the end.
If the bits of a variable are given twice, jMoped always takes the last one.
If w is an array, @PDSBits({"w=3", "w[]=1") means that the length of w has 3 bits (i.e. at most 7 elements), and each element of w has 1 bit.
The bits set by @PDSBits cannot be greater than the default bit in the progress view.
@PDSBits narrows down the scope of the analysis, which will make jMoped runs faster.

top

Question 4: What is the annotation @PDSArrayBits?

Answer: The annotaion @PDSArrayBits is used for specifying bits of array elements at class or method level. You will have to add pds.jar into your classpath, and import the class PDSArrayBits.

    import de.tum.in.jmoped.annotation.PDSArrayBits;

For example, by inserting

    @PDSArrayBits(1)

just before a class (or method) declaration means that the array elements will have just 1 bit for every array created in this class (or method).
Remark:

If both scopes are specified, the one at method level takes the priority.

top

Question 5: How to specify the bit sizes of a field?

Answer: See What is the annotation @PDSBits?. Alternatively, jMoped offers the annotations @PDSFieldBits exclusively for this purpose. You will have to add pds.jar into your classpath, and import the class PDSFieldBits.

    import de.tum.in.jmoped.annotation.PDSFieldBits;

It works as in the case of @PDSBits, but @PDSFieldBits takes an integer as the only argument. For example,

    @PDSFieldBits(2)
    int a;

the field a will have two bits.
Remark:

@PDSFieldBits always takes an integer as the only argument, and has no comma at the end.
If both @PDSBits and @PDSFieldBits are specified for the same field, @PDSFieldBits takes the priority.

top

Question 6: How to specify the bit sizes of a parameter?

Answer: See What is the annotation @PDSBits?. Alternatively, jMoped offers the annotations @PDSParameterBits exclusively for this purpose. You will have to add pds.jar into your classpath, and import the class PDSParameterBits.

    import de.tum.in.jmoped.annotation.PDSParameterBits;

It works as in the case of specifying parameter bits by sequence, i.e. put @PDSParameterBits just before method declarations and the sequence of integers tells which parameter has which bit.

    @PDSParameterBits({2, 3})
    void m(int x, int y)

The parameters x and y will have 2 and 3 bits, respectively.
Remark:

@PDSBits always takes an array of integers as the only argument, and has no comma at the end.
If both @PDSBits and @PDSParameterBits are specified for the same variable, @PDSParameterBits takes the priority.

top

Question 7: How to specify the bit sizes of a local variable?

Answer: See What is the annotation @PDSBits?.
Remark:

For technical reason, there is no @PDSLocalVariableBits, and it is not possible to write @PDSBits in front of a local variable.

top

Question 8: How does jMoped simulate Java heaps?

Answer: jMoped simulates the heap similar to the way JVM does. The simulation is achieved via a global array variable and a pointer. Every time a new object is created, it occupies some parts of the array. The pointer is always updated to the next available block of the array, which is determined by the size of the objects. For example, if the the heap size is 7, jMoped will declare

    int heap[7];
    int ptr;

top

Question 9: What is the option "Use one-bit heap"?

Answer: Instead of simulating a heap with an array of integers with default bits (see How does jMoped simulate Java heaps), this option uses an array of one-bit elements. For example, if the default bit size is 3 and the heap size is 7, the array will have 21 elements, where each element has one bit.

    int heap[21](1);

The heap pointer, on the other hand, does not increase with the heap size, but has the default bit size as in the normal case. The idea is that every time the pointer is used, it must always multiply by the default bit size. In other words, the pointer only points to the elements at the offsets of the default bit size, in this example only at the position 0, 3, 6, 9, ....

Integers are stored into the heap using bit-wise operators, e.g. the following codes store a into the heap at ptr, and updates the ptr to the next block

    heap[3*ptr] = a>>2, heap[3*ptr+1] = (a>>1)&1, heap[3*ptr+2] = a&1, ptr = ptr+1;

With this option jMoped utilizes the heap in a more efficient manner, however, it requires more time during its operation.

top