Package org.mpi_sws.jmc.api.util.concurrent

Class JmcAtomicInteger

java.lang.Object
org.mpi_sws.jmc.api.util.concurrent.JmcAtomicInteger
public class JmcAtomicInteger extends Object
A redefinition of AtomicInteger for JMC model checking. This class provides atomic operations on an integer value, ensuring thread safety through the use of a reentrant lock.

  • Constructor Summary

    Constructors
    Constructor
    Description
    JmcAtomicInteger()
    Constructs a new JmcAtomicInteger with an initial value of 0.
    JmcAtomicInteger(int initialValue)
    Constructs a new JmcAtomicInteger with the specified initial value.

  • Method Summary

    Modifier and Type
    Method
    Description
    int
    addAndGet(int delta)
    Atomically adds the given delta to the current value and returns the updated value.
    boolean
    compareAndSet(int expectedValue, int newValue)
    Atomically sets the value to the given updated value if the current value is equal to the expected value.
    int
    get()
    Returns the current value of this atomic integer.
    int
    getAndIncrement()
    Atomically increments the current value by 1 and returns the previous value.
    int
    getAndSet(int newValue)
    Atomically sets the value to the given new value and returns the previous value.
    void
    set(int newValue)
    Sets the value of this atomic integer to the given value.

    Methods inherited from class java.lang.Object

    clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

  • Constructor Details

    • JmcAtomicInteger

      public JmcAtomicInteger(int initialValue)
      Constructs a new JmcAtomicInteger with the specified initial value.
      Parameters:
      initialValue - the initial value of the atomic integer

    • JmcAtomicInteger

      public JmcAtomicInteger()
      Constructs a new JmcAtomicInteger with an initial value of 0.

  • Method Details

    • get

      public int get()
      Returns the current value of this atomic integer. Invokes a read event to the JMC runtime.
      Returns:
      the current value

    • set

      public void set(int newValue)
      Sets the value of this atomic integer to the given value. Invokes a write event to the JMC runtime.
      Parameters:
      newValue - the new value to set

    • compareAndSet

      public boolean compareAndSet(int expectedValue, int newValue)
      Atomically sets the value to the given updated value if the current value is equal to the expected value. Invokes a read followed by a write event to the JMC runtime.
      Parameters:
      expectedValue - the expected value
      newValue - the new value to set if the current value equals the expected value
      Returns:
      true if successful, false otherwise

    • getAndIncrement

      public int getAndIncrement()
      Atomically increments the current value by 1 and returns the previous value. Invokes a read followed by a write event to the JMC runtime.
      Returns:
      the previous value before incrementing

    • getAndSet

      public int getAndSet(int newValue)
      Atomically sets the value to the given new value and returns the previous value. Invokes a read followed by a write event to the JMC runtime.
      Parameters:
      newValue - the new value to set
      Returns:
      the previous value before setting the new value

    • addAndGet

      public int addAndGet(int delta)
      Atomically adds the given delta to the current value and returns the updated value. Invokes a read followed by a write event to the JMC runtime.
      Parameters:
      delta - the value to add
      Returns:
      the updated value after addition