Support for taking over the ownership of the collection/array/vararg

[jacek-lewandowski]

A simple example is as follows:

For the resources obtained outside

this works:

class Closeables implements Closeable {
  final @Owning Closeable res1;
  final @Owning Closeable res2;

  Closeables(@Owning r1, @Owning r2) {
    res1 = r1;
    res2 = r2;
  }
...
}

this does not work:

class Closeables implements Closeable {
  final @Owning Closeable[] res;

  Closeables(@Owning Closeable... r) {
    res = r;
  }
...
}

Is there a way to take over the ownership each item of a vararg / array / collection?

[kelloggm]

Is there a way to take over the ownership each item of a vararg / array / collection?

Unfortunately, no. This is a known limitation of the RLC; see further discussion here.

[msridhar]

@jacek-lewandowski we are actively brainstorming on how to add support for this. If you could link an example using an array of resources showing how they get closed it could be helpful to us.

[msridhar]

Also, for varargs, we do have the unchecked @EnsuresCalledMethodsVarArgs, docs here. This can be useful for utility routines like IOUtils.closeQuietly that are guaranteed to invoke close() on all of their arguments. But we do hope to have a way to actually check such routines in the future.

[jacek-lewandowski]

Thanks for the feedback! In Cassandra, indeed, we have methods that close multiple resources at once. For example, many of them are in the Throwables class (see https://github.com/apache/cassandra/blob/trunk/src/java/org/apache/cassandra/utils/Throwables.java#L215). I've tried using the @EnsuresCalledMethodsVarArgs annotation, and it helps for var-args, but it does not work with collections and often forces me to add suppression of contracts.postcondition.

Thanks for pointing me to the discussion. I'll follow it.

[msridhar]

One nasty issue we need to think through here is mutation. Consider:

class Closeables implements Closeable {
  final @Owning Closeable[] res;

  Closeables(@Owning Closeable... r) {
    res = r;
  }
  void update(@Owning Closeable c, int i) {
    // what should the verifier do about the old value in the array?
    res[i] = c;
  }
...
}

Similar issues arise for mutable collections. Possibly we need to prohibit such mutation for collections / arrays of @Owning pointers, but I'm not sure how. Need to think through this more and possibly study what Rust does for this kind of situation.

[jacek-lewandowski]

Maybe there could be an annotation which would mark a collection immutable?

[mernst]

Maybe there could be an annotation which would mark a collection immutable?

Several such exist (1, 2, 3, 4, 5), but none is shipped with the Checker Framework itself. One complication is aliasing (mutations through aliases).

[kelloggm]

Maybe there could be an annotation which would mark a collection immutable?

One complication is aliasing (mutations through aliases).

One option would be to trust rather than check an immutability annotation on collections, and let the RLC use that fact. Obviously, this is unsound, but it might be a good first step towards enabling us to verify ownership of resources by collections.

[jacek-lewandowski]

So I was trying to implement a resources map to be used to such situations, I have this:

@InheritableMustCall({ "removeAll" })
public class ResourcesMap<K, V>
{
    private final Map<K, V> map;

    public ResourcesMap()
    {
        this.map = new HashMap<>();
    }

    public @MustCallAlias V get(K key)
    {
        return map.get(key);
    }

    public @Owning V remove(K key)
    {
        return map.remove(key);
    }

    @CreatesMustCallFor
    public @MustCallAlias V put(K key, @Owning V value)
    {
        return map.put(key, value);
    }

    public void forEach(Consumer<@MustCallAlias V> consumer)
    {
        map.values().forEach(consumer);
    }

    public <T> void removeAll(T initial, OwningBiFunction<T, V> consumer)
    {
        Iterator<V> iterator = map.values().iterator();
        T acc = initial;
        while (iterator.hasNext())
        {
            V value = iterator.next();
            try
            {
                iterator.remove();
            }
            finally
            {
                acc = consumer.apply(acc, value);
            }
        }
    }

    public <T> void removeAll(OwningConsumer<V> consumer)
    {
        Iterator<V> iterator = map.values().iterator();
        while (iterator.hasNext())
        {
            V value = iterator.next();
            try
            {
                iterator.remove();
            }
            finally
            {
                consumer.accept(value);
            }
        }
    }

    public interface OwningConsumer<V> extends Consumer<V>
    {
        @Override
        void accept(@Owning V v);
    }

    public interface OwningBiFunction<T, V> extends BiFunction<T, V, T>
    {
        @Override
        T apply(T t, @Owning V v);
    }
}

which is used in the following way:

        ResourcesMap<TableId, UncommittedTableData.FlushWriter> flushWriters = new ResourcesMap<>();
        try (CloseableIterator<PaxosKeyState> iterator = updateSupplier.flushIterator(paxos))
        {
            while (iterator.hasNext())
            {
                PaxosKeyState next = iterator.next();
                UncommittedTableData.FlushWriter writer = flushWriters.get(next.tableId);
                if (writer == null)
                {
                    writer = getOrCreateTableState(next.tableId).flushWriter();
                    flushWriters.put(next.tableId, writer);
                }
                writer.append(next);
            }

            flushWriters.removeAll(UncommittedTableData.FlushWriter::finish);
        }
        catch (IOException t)
        {
            flushWriters.removeAll((Throwable) t, (acc, flushWriter) -> flushWriter.abort((acc)));
            throw new IOException(t);
        }

where the FlushWriter is something like:

    @InheritableMustCall({ "finish", "abort" })
    public interface FlushWriter
    {
        void append(PaxosKeyState commitState) throws IOException;

        void finish();

        Throwable abort(Throwable accumulate);

        default void appendAll(Iterable<PaxosKeyState> states) throws IOException
        {
            for (PaxosKeyState state : states)
                append(state);
        }
    }

Now, when I try to check it, it complains with the following:

    [javac] /home/jlewandowski/dev/cassandra/c18190-ecj/src/java/org/apache/cassandra/service/paxos/uncommitted/PaxosUncommittedTracker.java:161: error: [builder:required.method.not.called] @MustCall methods removeAll, finish, abort may not have been invoked on flushWriters or any of its aliases.
    [javac]         ResourcesMap<TableId, UncommittedTableData.FlushWriter> flushWriters = new ResourcesMap<>();
    [javac]                                                                 ^
    [javac]   The type of object is: org.apache.cassandra.utils.ResourcesMap<org.apache.cassandra.schema.TableId,org.apache.cassandra.service.paxos.uncommitted.UncommittedTableData.FlushWriter>.
    [javac]   Reason for going out of scope: possible exceptional exit due to throw new IOException(t); with exception type java.io.IOException

I'm not sure what I'm doing wrong there?

[msridhar]

@jacek-lewandowski this latest issue looks like a separate bug to me. I am not sure of the root cause. Could you file it as a distinct issue from this one?

[jacek-lewandowski]

sure, will do

[jacek-lewandowski]

#6054