A provably efficient algorithm for dynamic storage allocation