Feedback
Follow Us
Publication

Using lightweight formal methods to validate a key-value storage node in Amazon S3

By James Bornholt, Rajeev Joshi, Vytautas Astrauskas, Brendan Cully, Bernhard Kragl, Seth Markle, Kyle Sauri, Drew Schleit, Grant Slatton, Serdar Tasiran, Jacob Van Geffen, Andrew Warfield
2021
Download Copy BibTeX
Share
Download
Copy BibTeX
Share
This paper reports our experience applying lightweight formal methods to validate the correctness of ShardStore, a new key-value storage node implementation for the Amazon S3 cloud object storage service. By “lightweight formal methods" we mean a pragmatic approach to verifying the correctness of a production storage node that is under ongoing feature development by a full-time engineering team. We do not aim to achieve full formal verification, but instead emphasize automation, usability, and the ability to continually ensure correctness as both software and its specification evolve over time. Our approach decomposes correctness into independent properties, each checked by the most appropriate tool, and develops executable reference models as specifications to be checked against the implementation. Our work has prevented 16 issues from reaching production, including subtle crash consistency and concurrency problems, and has been extended by non-formal-methods experts to check new features and properties as ShardStore has evolved.
Research areas
Tags

Latest news

Work with us

See more jobs See more jobs
Applied Scientist, Sponsored Products Detail Page Blended Widgets
US, NY, New York
Amazon Advertising is one of Amazon's fastest growing and most profitable businesses. As a core product offering within our advertising portfolio, Sponsored Products (SP) helps merchants, retail vendors, and brand owners succeed via native advertising, which grows incremental sales of their products sold through Amazon. The SP team's primary goals are to help shoppers discover new products they love, be the most efficient way for advertisers to meet their business objectives, and build a sustainable business that continuously innovates on behalf of customers. Our products and solutions are strategically important to enable our Retail and Marketplace businesses to drive long-term growth. We deliver billions of ad impressions and millions of clicks and break fresh ground in product and technical innovations every day! The Detail Page Blended Widgets team is chartered with building novel product recommendation experiences. We push the innovation frontiers for our hundreds of millions of customers WW to aid product discovery while helping shoppers to find relevant products easily. Our team is building differentiated recommendations and utilizing cutting-edge machine learning techniques in the domain of natural language processing (NLP) and Transformer, deep learning, reinforcement learning, and Generative AI to provide delightful shopping experiences and deliver significant impact for the business. We are looking for an Applied Scientist who can delight our customers by continually learning and inventing. Our ideal candidate is an experienced Applied Scientist who has a track-record of performing deep analysis and is passionate about applying advanced ML and statistical techniques to solve real-world, ambiguous and complex challenges to optimize and improve the product performance, and who is motivated to achieve results in a fast-paced environment. The position offers an exceptional opportunity to grow your technical and non-technical skills and make a real difference to the Amazon Advertising business. As an Applied Scientist in the Blended Widgets team, you will: * Conduct hands-on data analysis, and run regular A/B experiments, gather data, perform statistical analysis and deep dive, and communicate the impact to senior management * Rapidly design, prototype and test many possible hypotheses in a high-ambiguity environment, making use of both quantitative analysis and business judgment * Establish scalable, efficient, automated processes for large-scale data analysis, machine-learning model development, model validation and serving * Collaborate with software engineering teams to integrate successful experimental results into large-scale, highly complex Amazon production systems * Promote the culture of experimentation and applied science at Amazon Team video https://youtu.be/zD_6Lzw8raE We are also open to consider the candidate in New York, or Seattle. We are open to hiring candidates to work out of one of the following locations: New York, NY, USA
Sr. Applied Scientist, Computer Vision
US, CA, Sunnyvale
We are looking for a passionate, talented Applied Scientists with a growth mindset who are adept at a variety of skills, especially with an array of Computer Vision and Machine Learning methods. Imagine being part of a team building the future of Smart Glasses. Echo Frames (Amazon’s first Smart Glasses product) is just the beginning. Amazon is focused on bringing technology and design into a form that is familiar to millions of people in a way that has never been done before. If you are excited about pushing the envelope and developing brand new experiences that empower users to do more as they engage with the physical world, we would love to meet you. You will have the opportunity to make impact across a couple of substantive organizations and be part of the start of a new product space within Amazon. Key job responsibilities This role is focused on developing performing, real-time Computer Vision and Machine Learning solutions and their associated deployment. You will develop core models that will be foundational of the key operational features that we are launching. You will conduct literature reviews to stay on the cutting edge of the field. You will regularly engage with product managers, software engineers, hardware engineers and stakeholders who will partner with you to guide and productize your work.- Drive end-to-end Computer Vision and Machine Learning methods that have a high degree of ambiguity, scale and complexity. - Build machine learning models, perform proof-of-concept, experiment, optimize, and deploy your models into production; work closely with software engineers and product managers to assist in productionizing your ML models. - Perform hands-on analysis on multi-sensor data sets to develop insights that drive product requirements. - Run A/B experiments, gather data, and perform statistical analysis. - Establish scalable, efficient, automated processes for data analysis, machine-learning model development, model validation and serving. - Research new and innovative sensor processing and Computer Vision approaches. - Mentor and help recruit Applied Scientists to the team. - Present results and explain methods to team leadership. - Write and pursue IP submissions. About the team Our team puts a high value on work-life balance. It isn’t about how many hours you spend at home or at work; it’s about how you bring energy to both parts of your life. We believe striking the right balance between your personal and professional life is critical to life-long happiness and fulfillment. We offer flexibility in working hours and encourage you to find your own balance between your work and personal lives. Our team is dedicated to supporting new members. We have a broad mix of experience levels and tenures, and we’re building an environment that celebrates knowledge sharing and mentorship. Our senior members enjoy one-on-one mentoring and thorough, but kind, code reviews. We care about your career growth and strive to assign projects based on what will help each team member develop into a better-rounded engineer and enable them to take on more complex tasks in the future. We are open to hiring candidates to work out of one of the following locations: Cupertino, CA, USA | Sunnyvale, CA, USA
Applied Scientist Intern, International Technology, 2024 Beijing
CN, 11, Beijing
职位：Applied scientist 应用科学家实习生 毕业时间：2024年10月 - 2025年9月之间毕业的应届毕业生 · 入职日期：2024年6月及之前 · 实习时间：保证一周实习4-5天全职实习，至少持续3个月 · 工作地点：北京朝阳区酒仙桥路恒通商务园区 · 校招信息请参考校园招聘申请手册： https://amazonexteu.qualtrics.com/CP/File.php?F=F_55YI0e7rNdeoB6e 投递须知： 1 填写简历申请时，请把必填和非必填项都填写完整。提交简历之后就无法修改了哦！ 2 学校的英文全称请准确填写。 如果您正在攻读NLP，IR或搜索领域专业的博士或硕士研究生，而且对应用科学家的实习工作感兴趣。如果您也喜爱深入研究棘手的技术问题并提出解决方案，用成功的产品显著地改善人们的生活。 那么，我们诚挚邀请您加入亚马逊的International Technology搜索团队改善Amazon的产品搜索服务。我们的目标是帮助亚马逊的客户找到他们所需的产品，并发现他们感兴趣的新产品。 这会是一份收获满满的工作。您每天的工作都与全球数百万亚马逊客户的体验紧密相关。您将提出和探索NLP和IR领域的创新，基于TB级别的产品和流量数据设计机器学习模型。您将集成这些模型到搜索引擎中为客户提供服务，通过数据，建模和客户反馈来完成闭环。您对模型的选择需要能够平衡业务指标和响应时间的需求。 We are open to hiring candidates to work out of one of the following locations: Beijing, 11, CHN
Amazon Robotics - Data Scientist, Global Services and Support
US, MA, Boston
Are you inspired by invention? Is problem solving through teamwork in your DNA? Do you like the idea of seeing how your work impacts the bigger picture? Answer yes to any of these and you’ll fit right in here at Amazon Robotics. We are a smart team of doers that work passionately to apply cutting edge advances in robotics and software to solve real-world challenges that will transform our customers’ experiences in ways we can’t even imagine yet. We invent new improvements every day. We are Amazon Robotics and we will give you the tools and support you need to invent with us in ways that are rewarding, fulfilling and fun. Amazon Robotics, a wholly owned subsidiary of Amazon.com, empowers a smarter, faster, more consistent customer experience through automation. Amazon Robotics automates fulfillment center operations using various methods of robotic technology including autonomous mobile robots, sophisticated control software, language perception, power management, computer vision, depth sensing, machine learning, object recognition, and semantic understanding of commands. Amazon Robotics has a dedicated focus on research and development to continuously explore new opportunities to extend its product lines into new areas. AR is seeking uniquely talented and motivated data scientists to join our Global Services and Support (GSS) Tools Team. GSS Tools focuses on improving the supportability of the Amazon Robotics solutions through automation, with the explicit goal of simplifying issue resolution for our global network of Fulfillment Centers. The candidate will work closely with software engineers, Fulfillment Center operation teams, system engineers, and product managers in the development, qualification, documentation, and deployment of new - as well as enhancements to existing - operational models, metrics, and data driven dashboards. As such, this individual must possess the technical aptitude to pick-up new BI tools and programming languages to interface with different data access layers for metric computation, data mining, and data modeling. Key job responsibilities If you are not sure that every qualification on the list above describes you exactly, we'd still love to hear from you! At Amazon, we value people with unique backgrounds, experiences, and skillsets. If you’re passionate about this role and want to make an impact on a global scale, please apply! Amazon offers a full range of benefits that support you and eligible family members, including domestic partners and their children. Benefits can vary by location, the number of regularly scheduled hours you work, length of employment, and job status such as seasonal or temporary employment. The benefits that generally apply to regular, full-time employees include: 1. Medical, Dental, and Vision Coverage 2. Maternity and Parental Leave Options 3. Paid Time Off (PTO) 4. 401(k) Plan We are open to hiring candidates to work out of one of the following locations: Boston, MA, USA
Senior Applied Scientist, Global Reliability, Maintenance & Engineering, Decision Science and Technology
LU, Luxembourg
Are you a talented and inventive scientist with strong passion about AI applications? Would you like to develop machine learning and optimization tools by playing a key role in the Decision Science and Technology (DST) team within the Global RME Central organization? Our mission is to leverage the use of data, science, and technology to improve the efficiency of RME maintenance activities, reduce costs, increase safety and promote sustainability while creating frictionless customer experiences. As Applied Scientist in DST you will be focused on leading the design and development of innovative approaches and solutions by leading technical work supporting RME’s Predictive Maintenance (PdM) and Spare Parts (SP) programs. You will connect with world leaders in your field and you will be tackling customer's natural language challenges by carrying out a systematic review of existing solutions. The appropriate choice of AI methods and their deployment into effective tools will be the key for the success in this role. The successful candidate will be a self-starter comfortable with ambiguity, with strong attention to detail and outstanding ability in balancing technical leadership with strong business judgment to make the right decisions about model and method choices. Key job responsibilities - Provide technical expertise to support team strategies that will take EU RME towards World Class predictive maintenance practices and processes, driving better equipment up-time and lower repair costs with optimized spare parts inventory and placement - Implement an advanced maintenance framework utilizing Machine Learning technologies to drive equipment performance leading to reduced unplanned downtime - Provide technical expertise to support the development of long-term spares management strategies that will ensure spares availability at an optimal level for local sites and reduce the cost of spares We are open to hiring candidates to work out of one of the following locations: Luxembourg, LUX
Applied Scientist, Ad Measurements Science
CA, ON, Toronto
Amazon Advertising is one of Amazon's fastest growing and most profitable businesses, responsible for defining and delivering a collection of advertising products that drive discovery and sales. Our products and solutions are strategically important to enable our Retail and Marketplace businesses to drive long-term growth. We deliver billions of ad impressions and millions of clicks and break fresh ground in product and technical innovations every day! The Measurement Science team delivers campaign measurement and reporting across Amazon Advertising businesses and serves as the scientific center of excellence for algorithm development in campaign measurement. Programs supported by our services include Sponsored Products, Sponsored Brands, Sponsored Display, Amazon DSP for Display, Video and Audio advertising, 3P Paid Merchandising (HOTW), Amazon Live, and others. Our measurement engineering platforms and products deliver campaign performance reporting to advertisers. This includes development and management of: our compute infrastructure; ad server logs, identities, conversion events, and campaign dimension ingestion; advertising facts aggregation at scale; attribution processing; measurement of complex campaign calculations such as unique reach and frequency; interactive dash-boarding infrastructure; campaign reporting applications for display advertising programs; and data warehousing of advertising aggregates for business intelligence. We show ads on and off our site, effectively measuring the internet with billions of incoming, highly decorated events to process and summarize every day in near real time. Our infrastructure is extreme scale, requiring invention ahead of common technologies and exceeding the scale of most of Amazon services (>1mm TPS, PB-scale). Key job responsibilities * Drive end-to-end Machine Learning projects that have a high degree of ambiguity, scale, complexity. * Perform hands-on analysis and modeling of enormous data sets to develop insights that increase traffic monetization and merchandise sales, without compromising the shopper experience. * Build machine learning models, perform proof-of-concept, experiment, optimize, and deploy your models into production; work closely with software engineers to assist in productionizing your ML models. * Run A/B experiments, gather data, and perform statistical analysis. * Establish scalable, efficient, automated processes for large-scale data analysis, machine-learning model development, model validation and serving. * Research new and innovative machine learning approaches. * Recruit Scientists to the team and provide mentorship. You will invent new experiences and influence customer-facing shopping experiences to help suppliers grow their retail business and the auction dynamics that leverage native advertising; this is your opportunity to work within the fastest-growing businesses across all of Amazon! Define a long-term science vision for our advertising business, driven from our customers' needs, translating that direction into specific plans for scientists, as well as engineering and product teams. This role combines science leadership, organizational ability, technical strength, product focus, and business understanding. A day in the life About the team Amazon is investing heavily in building a world-class advertising business. This team defines and delivers a collection of advertising products that drive discovery and sales. Our solutions generate billions in revenue and drive long-term growth for Amazon’s Retail and Marketplace businesses. We deliver billions of ad impressions, millions of clicks daily, and break fresh ground to create world-class products. We are a highly motivated, collaborative, and fun-loving team with an entrepreneurial spirit - with a broad mandate to experiment and innovate. Team video https://youtu.be/zD_6Lzw8raE We are open to hiring candidates to work out of one of the following locations: Toronto, ON, CAN
Applied Scientist, Sponsored Products - Auction
US, NY, New York
Amazon is investing heavily in building a world class advertising business and we are responsible for defining and delivering a collection of self-service performance advertising products that drive discovery and sales. Our products are strategically important to our Retail and Marketplace businesses driving long term growth. We deliver billions of ad impressions and millions of clicks daily and are breaking fresh ground to create world-class products. We are highly motivated, collaborative and fun-loving with an entrepreneurial spirit and bias for action. With a broad mandate to experiment and innovate, we are growing at an unprecedented rate with a seemingly endless range of new opportunities. We are looking for a Data Scientist/Applied Scientist to join Search Product Discovery team in Marketplace Intelligence with a broad mandate to experiment and innovate to grow Sponsored Products. As an Applied Scientist in this team, you will help to identify unique opportunities to create customized and delightful shopping experience for our growing marketplaces worldwide. You will play a crucial role in enriching the diversity of Amazon's search page to improve the shopping experience for our customers. Your primary focus will be harnessing your analytical skills to establish diversity metrics, conduct in-depth research into how diversity influences shopper behavior, and construct a comprehensive framework to enhance product diversity through ad ranking and allocation on the search page. Key job responsibilities - Be the technical leader in statistical methods and Machine Learning; lead efforts within this team and across other teams. - Perform hands-on analysis and modeling of enormous data sets to develop insights that increase traffic monetization and merchandise sales, without compromising the shopper experience. - Drive end-to-end Machine Learning projects that have a high degree of ambiguity, scale, complexity. - Run A/B experiments, gather data, and perform statistical analysis. - Establish scalable, efficient, automated processes for large-scale data analysis, machine-learning model development, model validation and serving. - Research new and innovative machine learning approaches. - Recruit Scientists to the team and provide mentorship. We are open to hiring candidates to work out of one of the following locations: New York, NY, USA
Data Science Manager, Amazon B2B Payments and Lending
US, NY, New York
The Data Science Manager will be a key leadership member the Credit team in Amazon Business Payments and Lending. This leader will lead the science team developing best-in-class underwriting systems. This role presents a significant intellectual, technical, and operational challenge with enormous opportunity for business impact. Amazon is dedicated to building credit/lending services that help small, medium, and large businesses worldwide. We believe we are in a unique position to serve our customers with exceptional value due to our deep understanding and insight into our base coupled with rigorous scientific approach and customer-focused emphasis to building financial products. This leader will be passionate about enabling the growth of small, medium, and large businesses and other to-be-launched segments by removing a critical barrier to deepening their activity on Amazon – access to capital. This leader will demonstrate high judgment and deep business experience across economic cycles. They will bring proven ability to identify and recommend data-driven solutions, navigating through complex financial and regulatory issues across geographies. This role is highly strategic and will interact with all levels across a broad range of teams and leaders across Amazon. This leader will need to work with our business and product management partners to communicate the properties of their team’s analysis/modeling. This leader owns the multi-year research agenda and prioritization for the team, and ensure that projects meaningful drive results. Key job responsibilities · Lead, mentor, and develop a top-performing data science team · Apply advanced analytics and ML techniques to support Credit Management processes · Source, incorporate, and analyze alternative credit data to drive innovation · Own data science team roadmap, balance multiple projects efficiently and achieve goals in a fast-paced, dynamic environment · Collaborate effectively with Credit Strategy, operation, product teams, and senior management at ABPL to underwrite new customers and manage portfolio risk · Enhance operating efficiencies and excellence, ensure high performant credit management science models · Promote a culture of transparency, integrity, and ethical use of data. We are open to hiring candidates to work out of one of the following locations: New York, NY, USA | Seattle, WA, USA
Applied Scientist, AWS
IN, KA, Bangalore
The Generative AI Innovation Center team at AWS provides opportunities to innovate in a fast-paced organization that contributes to game-changing projects and technologies leveraging cutting-edge generative AI algorithms. As an Applied Scientist, you'll partner with technology and business teams to build solutions that surprise and delight our customers. We’re looking for Applied Scientists capable of using generative AI and other ML techniques to design, evangelize, and implement state-of-the-art solutions for never-before-solved problems. Here at AWS, we welcome all builders. We believe that technology should be built in a way that’s inclusive, accessible, and equitable. We’re committed to putting in the work for more equal representation Key job responsibilities * Collaborate with scientists and engineers to research, design and develop cutting-edge generative AI algorithms to address real-world challenges * Work across customer engagement to understand what adoption patterns for generative AI are working and rapidly share them across teams and leadership * Interact with customers directly to understand the business problem, help and aid them in implementation of generative AI solutions, deliver briefing and deep dive sessions to customers and guide customer on adoption patterns and paths for generative AI * Create and deliver best practice recommendations, tutorials, blog posts, sample code, and presentations adapted to technical, business, and executive stakeholder * Provide customer and market feedback to Product and Engineering teams to help define product direction. About the team You will work with a diverse team of Architects, ML Scientists, and Strategists to help and guide AWS customers across Asia Pacific, Japan, China and India in their journey to adopt generative AI. We are open to hiring candidates to work out of one of the following locations: Bangalore, KA, IND | Mumbai, MH, IND
Applied Scientist Intern (Computer Vision algorithms), Amazon Lab126, Taiwan
TW, TPE, Taipei
Amazon Lab126 is an inventive research and development company that designs and engineers high-profile consumer electronics. Lab126 began in 2004 as a subsidiary of Amazon.com, Inc., originally creating the best-selling Kindle family of products. Since then, we have produced groundbreaking devices like Fire tablets, Fire TV, and Amazon Echo. What will you help us create? Key job responsibilities You will be working on developing Computer Vision algorithms to improve deep learning models including reducing the sample complexity, improving generalization ability, boosting model robustness, etc. You will be a critical science contributor and can create a significant business impact to the company. This opportunity requires excellent technical, problem-solving, and communication skills. An ideal candidate will have a high teamwork mentality coupled with a strong bias for action yet always insisting on the highest standards. We also aim to publish our innovation and findings to computer vision top conferences including CVPR, ICCV, ECCV. A day in the life In this role, you will work closely with other researchers in the team to research, design, and deliver science components powering computer vision and active learning algorithms to cost-effectively create very large-scale training datasets for various computer vision/robotics applications. You will have the unique opportunity to work on multiple popular Computer Vision tasks altogether, therefore, embrace the great potential to innovate more. About the team We are a smart team of doers that work passionately to apply cutting-edge advances in robotics and software to solve real-world challenges that will transform our customers’ experiences in ways we can’t even imagine yet. The team is using computer vision, machine learning, sensor fusion, real-time and distributed systems to convert requirements into concrete deliverables. A Researcher on this team will translate business and functional requirements into working code. Comfort with a high degree of ambiguity and ability to solve problems that haven’t been solved to scale before are essential. We are open to hiring candidates to work out of one of the following locations: Hsinchu City, TPE, TWN | Taipei, TPE, TWN
View from space of a connected network around planet Earth representing the Internet of Things.
Have feedback?
Let us know by taking this short survey
Get started
Amazon.com | Conditions of Use | Privacy | © 1996-2023 Amazon.com, Inc. or its affiliates
Follow Us