As part of your project, you need to call a third party API. There are two types of calls you need to make:
There is a known rate limit of N calls per unit of time on this API, and you do not want to exceed this. The first type may make an arbitrary number of calls, but it’s less critical and you are comfortable waiting between calls. For the second, it will make either 1 or 2 calls; however, being higher priority, you want to immediately update the object if necessary. With these constraints in mind, how do you guarantee you never exceed the rate limit?
We start with the minimum possible case.
---- MODULE api ----
EXTENDS Integers, TLC
(* --algorithm api
variables made_calls = 0, max_calls \in 5..10;
macro make_calls(n)
begin
made_calls := made_calls + n;
assert made_calls <= max_calls;
end macro;
process get_collection = 0
begin
Request:
make_calls(1);
either goto Request
or skip
end either;
end process;
process get_put \in 1..3
begin
Call:
with c \in {1, 2} do
make_calls(c)
end with;
end process;
end algorithm; *)
====
Since most of the business logic is irrelevant to our use case, we simply leave it out. get_collection makes an arbitrary number of calls, represented by the either goto. Every time TLC reaches that branch point it will explore both branches, so we know this can be an arbitrary number of calls. Similarly, the get_put makes either one or two calls in a transaction. Finally, every time the made_calls changes we check that we haven’t gone over the maximum.
If we run this, we’ll get an error: the assert fails pretty trivially. We can fix this by adding a check in the macro, so that we only make a call if we have enough rate left. One fix is this:
macro make_calls(n)
begin
if made_calls <= max_calls - n then
made_calls := made_calls + n;
assert made_calls <= max_calls;
end if;
end macro;
Which makes the call fail silently if it would take us past the limit.
Our solution works, but misses the business case: we don’t want to not make the calls, we want to wait on them until the rate limit refreshes. We can simulate that with an await:
macro make_calls(n)
begin
await made_calls <= max_calls - n;
made_calls := made_calls + n;
assert made_calls <= max_calls;
end macro;
If we run this, though, we get a deadlock. That’s because all of our processes are waiting for the limit to refresh, which we never actually coded. Here’s one way of doing this:
process reset_limit = -1
begin
Reset:
while TRUE do
made_calls := 0;
end while
end process
If we add that, the spec passes as normal.
Let’s add a complication: all of the processes are running on different workers, so they don’t automatically know the number of calls made. In order to avoid going past the limit, we need to share that information, which takes time. One way we can do this is by having each process query a central cache that only move forward if there’s enough calls remaining. One representation would be
EXTENDS Integers, TLC
(* --algorithm api
variables made_calls = 0, max_calls \in 5..10;
macro make_calls(n)
begin
made_calls := made_calls + n;
assert made_calls <= max_calls;
end macro;
process reset_limit = -1
begin
Reset:
while TRUE do
made_calls := 0;
end while
end process
process get_collection = 0
begin
GCGetCalls:
await made_calls <= max_calls - 1;
Request:
make_calls(1);
either goto GCGetCalls
or skip
end either;
end process;
process get_put \in 1..3
begin
GPGetCalls:
await made_calls <= max_calls - 2;
Call:
with c \in {1, 2} do
make_calls(c)
end with;
end process;
end algorithm; *)
=========
When we run this, we see it fails, as between the get and the request another process can make a call. If we want to resolve this we need some form of locking or priority. This will work, but it also explodes the diameter. Every process needs to wait on every other process, even when there’s plenty of calls to go around. We should instead look for a more optimized way of handling this issue.
One solution we can use is to reserve calls: when a process checks that there are calls remaining, it reserves N calls that are considered made in our cache but not in the API endpoint. Then, once we make the appropriate calls, we return the necessary reserves.
---- MODULE api ----
EXTENDS Integers, TLC
(* --algorithm api
variables made_calls = 0, max_calls \in 5..10, reserved_calls = 0;
macro make_calls(n) begin
made_calls := made_calls + n;
assert made_calls <= max_calls;
end macro;
macro reserve(n) begin
await made_calls + reserved_calls + n <= max_calls;
reserved_calls := reserved_calls + n;
end macro
process reset_limit = -1
begin
Reset:
while TRUE do
made_calls := 0;
end while
end process
process get_collection = 0
begin
GCGetCalls:
reserve(1);
Request:
make_calls(1);
reserved_calls := reserved_calls - 1;
either goto GCGetCalls
or skip
end either;
end process;
process get_put \in 1..3
begin
GPGetCalls:
reserve(2);
Call:
with c \in {1, 2} do
make_calls(c)
end with;
reserved_calls := reserved_calls - 2;
end process;
end algorithm; *)